theory Bash
imports Pure
keywords "CD" :: thy_decl
  and "PWD" "bash" :: diag
begin

ML {*
structure CD = Theory_Data
(
  type T = Path.T;
  val empty = Path.current;
  fun extend _ = empty;
  fun merge _ = empty;
)
*}

ML {*
  fun pwd thy = writeln (Path.print (CD.get thy));

  Outer_Syntax.improper_command @{command_spec "PWD"}
    "print current working directory of theory context"
    (Scan.succeed (Toplevel.keep (fn st => pwd (Toplevel.theory_of st))));

  Outer_Syntax.improper_command @{command_spec "CD"}
    "change current working directory within theory"
    (Parse.path >> (fn name =>
      Toplevel.theory (CD.put (Path.expand (Path.explode name)) #> tap pwd)));

  Outer_Syntax.improper_command @{command_spec "bash"}
    "invoke GNU Bourne Again Shell command-line, relatively to working directory of theory"
    (Parse.name >> (fn cmd =>
      Toplevel.keep (fn st =>
        let
          val cd = CD.get (Toplevel.theory_of st);
          val rc = Isabelle_System.bash ("cd " ^ File.shell_path cd ^ "; " ^ cmd)
        in writeln (string_of_int rc) end)));
*}

CD "~"
bash "ls -al"

CD "~~"
bash "ls -al"

CD "$ISABELLE_HOME_USER"
bash "ls -al"

end