Sketch implementation of facility to handle script chunks

mn200 · mn200 · commit ec2580f47550 · 2026-01-12T16:55:57.000+11:00
This should let various editor modes share standard facilities for loading dependencies etc. Work for github issue #1767
diff --git a/src/parse/ReplCommands.sig b/src/parse/ReplCommands.sig
@@ -0,0 +1,40 @@
+signature ReplCommands =
+sig
+
+(* Facilities for turning chunks of script file text into commands that can
+   be fed to running REPL instances.
+
+   Editor is responsible for detecting/selecting the relevant text but does
+   not need to examine it further. Instead, it can feed, for example
+
+    ReplCommands.execute_command (sml_text (...,{filename=...,text =...}));
+
+   to the running session.  The ...s above correspond solely to trivially
+   derived information about where and what the text is.  The editor needs to
+   know to use temporary files to stash particularly huge bits of text, using
+   the ViaFile constructor to the string_src type rather than writing huge
+   string literals into the REPL.
+
+   If the parsing of text into commands fails, the functions will put their
+   errors into the Failure constructor and the execute_command can then get the
+   REPL to emit the appropriate diagnostics.
+
+*)
+
+datatype string_src = Direct of string | ViaFile of {proxy_filename : string}
+type script_text = locn.locn * {filename : string option, text : string_src}
+
+datatype repl_command = Success of string | Failure of string
+
+val sml_text : script_text -> repl_command
+val set_initial_goal : script_text -> repl_command
+val set_by_subgoal : script_text -> repl_command
+val set_suffices_by_subgoal : script_text -> repl_command
+val apply_tactic : script_text -> repl_command
+val apply_tactic_pattern : script_text -> repl_command
+  (* tactic patterns as per the second argument to the >~ operator *)
+val load_dependencies : script_text -> repl_command
+
+val execute_command : repl_command -> unit
+
+end
diff --git a/src/parse/ReplCommands.sml b/src/parse/ReplCommands.sml
@@ -0,0 +1,28 @@
+structure ReplCommands :> ReplCommands =
+struct
+
+
+datatype string_src = Direct of string | ViaFile of {proxy_filename : string}
+type script_text = locn.locn * {filename : string option, text : string_src}
+
+datatype repl_command = Success of string | Failure of string
+
+fun sml_text s = Failure "Unimplemented"
+fun set_initial_goal s = Failure "Unimplemented"
+fun set_by_subgoal s = Failure "Unimplemented"
+fun set_suffices_by_subgoal s = Failure "Unimplemented"
+fun apply_tactic s = Failure "Unimplemented"
+fun apply_tactic_pattern s = Failure "Unimplemented"
+fun load_dependencies s = Failure "Unimplemented"
+
+(* Under Moscow ML, handling a Success will require writing the string to a
+   file and then use-ing it.  Error-reporting will be poor; under Poly/ML the
+   compiler can be invoked more directly, with line-numbers set up
+   appropriately. *)
+fun execute_command rc =
+    case rc of
+        Failure s => print s
+      | Success s => print "Can't do anything yet"
+
+
+end
