Re: [isabelle] I need an ML function to get the THY path and filename

On Mon, 31 Mar 2014, Gottfried Barrow wrote:

The key word is "internal". When the PIDE is powered up, the goal is to stay working internal to a THY and the related THY and ML files, as much as possible. I click on a cntl-hover link to get me files.


I access Unix essentials in the THY, viewing results in the output panel, not having to resort to the Console, which will allow me to create a history of commands.

I attach a screenshot and THY to show I'm one, small step closer to the end result.

I don't know what the end result will be, but here is my contribution to the game: Bash.thy with CD, PWD, and bash commands inside the theory context. Note that I could not use the names "cd" and "pwd", since these are left-over commands from ancient times.

The global working directory of a process (e.g. is incompatible with the idea of stateless execution. By putting the cd value into the formal context, you can feed that to each shell process individually, and they can run in parallel unencumbered. This is done by the PIDE automatically, since the 'bash' command is diagnostic and thus mean to be without any effects.

Of course, unpredictable or really bad things will happen, when you modify the file system in any of these bash commands.

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

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"
    ( >> (fn cmd =>
      Toplevel.keep (fn st =>
          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"

bash "ls -al"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.