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.*
# HG changeset patch # User Simon Foster <[email protected]> # Date 1626868953 -3600 # Wed Jul 21 13:02:33 2021 +0100 # Node ID a601e4bfab9bf3f7c38750a2f2b8475b0d0197c8 # Parent 7e2a9a8c2b85f10d81f3be433878fe51fa13eb6f Added active markup elements and functions for running commands in the jEdit console plugin diff -r 7e2a9a8c2b85 -r a601e4bfab9b src/Pure/PIDE/active.ML --- a/src/Pure/PIDE/active.ML Sat Feb 20 13:42:37 2021 +0100 +++ b/src/Pure/PIDE/active.ML Wed Jul 21 13:02:33 2021 +0100 @@ -14,6 +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 end; structure Active: ACTIVE = @@ -60,5 +62,10 @@ (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_system_shell_command cmd = run_shell_command "System" cmd; + end; diff -r 7e2a9a8c2b85 -r a601e4bfab9b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Feb 20 13:42:37 2021 +0100 +++ b/src/Pure/PIDE/markup.ML Wed Jul 21 13:02:33 2021 +0100 @@ -210,6 +210,9 @@ val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string + val run_shell_commandN: string + val shell_commandN: string + val shell_typeN: string val functionN: string val ML_statistics: {pid: int, stats_dir: string} -> Properties.T val commands_accepted: Properties.T @@ -670,6 +673,11 @@ val jedit_actionN = "jedit_action"; +val run_shell_commandN = "run_shell_command" + +val shell_commandN = "shell_command" + +val shell_typeN = "shell_type" (* protocol message functions *) diff -r 7e2a9a8c2b85 -r a601e4bfab9b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Feb 20 13:42:37 2021 +0100 +++ b/src/Pure/PIDE/markup.scala Wed Jul 21 13:02:33 2021 +0100 @@ -578,6 +578,9 @@ val JEDIT_ACTION = "jedit_action" + val SHELL_COMMAND = "shell_command" + val SHELL_TYPE = "shell_type" + val RUN_SHELL_COMMAND = "run_shell_command" /* protocol message functions */ diff -r 7e2a9a8c2b85 -r a601e4bfab9b src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Feb 20 13:42:37 2021 +0100 +++ b/src/Pure/PIDE/rendering.scala Wed Jul 21 13:02:33 2021 +0100 @@ -219,7 +219,7 @@ val active_elements = Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS, - Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) + Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL, Markup.RUN_SHELL_COMMAND) val background_elements = Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE + diff -r 7e2a9a8c2b85 -r a601e4bfab9b src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Sat Feb 20 13:42:37 2021 +0100 +++ b/src/Tools/jEdit/src/active.scala Wed Jul 21 13:02:33 2021 +0100 @@ -9,7 +9,7 @@ import isabelle._ import org.gjt.sp.jedit.{ServiceManager, View} - +import console.{Console, Shell} object Active { @@ -103,6 +103,27 @@ model.session.dialog_result(id, serial, result) true + case XML.Elem(Markup(Markup.RUN_SHELL_COMMAND, props), _) => + val shell_name = Properties.get(props, Markup.SHELL_TYPE).getOrElse("System") + Properties.get (props, Markup.SHELL_COMMAND) match { + case None => false + case Some(cmd) => + view.getDockableWindowManager().addDockableWindow("console") + + // Obtain the console instance + val console = view.getDockableWindowManager().getDockable("console").asInstanceOf[Console] + + // Set the shell to use + val shell = Shell.getShell(shell_name) + + shell.stop(console) + while (!shell.waitFor(console)) { } + console.run(shell, cmd) + + true + } + + case _ => false } }
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
