Hi all, Just a brief update on this. I've added the ability to pass a new working directory to, which causes the shell to switch directory prior to running the command. A patch increment to the previous one is attached.
Regards, Simon. On Wed, 21 Jul 2021 at 13:23, Simon Foster <[email protected]> wrote: > Dear Isabelle Developers, > > I've had a first go at developing a PIDE active area that integrates with > the jEdit console plugin. This is essentially a new Markup element called > "run_shell_command" that can be used to execute a command in a target > console. There's also a new Isabelle/ML function > Active.run_shell_command: string -> string -> string -> string, which takes > a target shell (e.g. "System", "Scala" etc.), a command to execute, and a > message to display. If printed with writelen, the markup produces an active > area in the Output pane that switches focus to the Console pane, and given > Shell, and runs the given command. For example, > > writeln (Active.run_shell_command "System" "ghci" "Start GHCi") > > An envisaged use case is use of external interpreters, such as GHCi, to > execute code and other exported artifacts. A patch wrt. to the Isabelle > development repository, adding the above functionality, is attached. I'd be > happy to receive any feedback or suggested changes on this. > > Regards, > > Simon. > > -- > Dr. Simon Foster - Research Fellow in Computer Science > High Integrity Systems Engineering Group, University of York > http://www.cs.york.ac.uk/~simonf > > *My normal working hours are 8:30am to 4:30pm Monday to Friday.* > -- Dr. Simon Foster - Research Fellow in Computer Science High Integrity Systems Engineering Group, University of York http://www.cs.york.ac.uk/~simonf *My normal working hours are 8:30am to 4:30pm Monday to Friday.*
# HG changeset patch # User Simon Foster <[email protected]> # Date 1626952320 -3600 # Thu Jul 22 12:12:00 2021 +0100 # Node ID 7397b4bf6b65a8d730d644df236d321f5ee691b5 # Parent a601e4bfab9bf3f7c38750a2f2b8475b0d0197c8 Extended the run_shell_command active area so that it can change to a directory diff -r a601e4bfab9b -r 7397b4bf6b65 ROOTS --- a/ROOTS Wed Jul 21 13:02:33 2021 +0100 +++ b/ROOTS Thu Jul 22 12:12:00 2021 +0100 @@ -10,4 +10,4 @@ src/Sequents src/Doc src/Tools - +/home/simonfoster/Isabelle diff -r a601e4bfab9b -r 7397b4bf6b65 src/Pure/PIDE/active.ML --- a/src/Pure/PIDE/active.ML Wed Jul 21 13:02:33 2021 +0100 +++ b/src/Pure/PIDE/active.ML Thu Jul 22 12:12:00 2021 +0100 @@ -14,8 +14,8 @@ val dialog: unit -> (string -> Markup.T) * string future val dialog_text: unit -> (string -> string) * string future val dialog_result: serial -> string -> unit - val run_shell_command: string -> string -> string -> string - val run_system_shell_command: string -> string -> string + val run_shell_command: string -> string option -> string -> string -> string + val run_system_shell_command: string option -> string -> string -> string end; structure Active: ACTIVE = @@ -62,10 +62,15 @@ (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab)) |> (fn NONE => () | SOME promise => Future.fulfill promise result); -fun run_shell_command shell cmd = - Markup.markup (make_markup Markup.run_shell_commandN {implicit = false, properties = [(Markup.shell_typeN, shell), (Markup.shell_commandN, cmd)]}); +fun run_shell_command shell dir cmd = + let val dirprop = (case dir of NONE => [] | SOME d => [(Markup.shell_directoryN, d)]) + in Markup.markup + (make_markup Markup.run_shell_commandN + {implicit = false + ,properties = [(Markup.shell_typeN, shell), (Markup.shell_commandN, cmd)] @ dirprop}) + end -fun run_system_shell_command cmd = run_shell_command "System" cmd; +val run_system_shell_command = run_shell_command "System"; end; diff -r a601e4bfab9b -r 7397b4bf6b65 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Jul 21 13:02:33 2021 +0100 +++ b/src/Pure/PIDE/markup.ML Thu Jul 22 12:12:00 2021 +0100 @@ -213,6 +213,7 @@ val run_shell_commandN: string val shell_commandN: string val shell_typeN: string + val shell_directoryN: string val functionN: string val ML_statistics: {pid: int, stats_dir: string} -> Properties.T val commands_accepted: Properties.T @@ -679,6 +680,8 @@ val shell_typeN = "shell_type" +val shell_directoryN = "shell_directory" + (* protocol message functions *) val functionN = "function" diff -r a601e4bfab9b -r 7397b4bf6b65 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Jul 21 13:02:33 2021 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Jul 22 12:12:00 2021 +0100 @@ -580,6 +580,7 @@ val SHELL_COMMAND = "shell_command" val SHELL_TYPE = "shell_type" + val SHELL_DIRECTORY = "shell_directory" val RUN_SHELL_COMMAND = "run_shell_command" /* protocol message functions */ diff -r a601e4bfab9b -r 7397b4bf6b65 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Wed Jul 21 13:02:33 2021 +0100 +++ b/src/Tools/jEdit/src/active.scala Thu Jul 22 12:12:00 2021 +0100 @@ -118,6 +118,15 @@ shell.stop(console) while (!shell.waitFor(console)) { } + + // Change directory if requested + Properties.get(props, Markup.SHELL_DIRECTORY) match { + case Some(dir) => shell.chDir(console, dir); + case None => {} + } + while (!shell.waitFor(console)) { } + + // Run the given command console.run(shell, cmd) true
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
