--- a/etc/options Sun May 24 09:04:25 2020 +0200
+++ b/etc/options Sun May 24 21:11:23 2020 +0200
@@ -150,7 +150,7 @@
section "PIDE Build"
-option pide_build : bool = false
+option pide_session : bool = false
-- "build session heaps via PIDE"
option pide_reports : bool = true
--- a/etc/settings Sun May 24 09:04:25 2020 +0200
+++ b/etc/settings Sun May 24 21:11:23 2020 +0200
@@ -23,6 +23,8 @@
isabelle_scala_service 'isabelle.Tools'
[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
+isabelle_scala_service 'isabelle.Functions'
+
isabelle_scala_service 'isabelle.Bibtex$File_Format'
#paranoia settings -- avoid intrusion of alien options
--- a/etc/symbols Sun May 24 09:04:25 2020 +0200
+++ b/etc/symbols Sun May 24 21:11:23 2020 +0200
@@ -417,6 +417,8 @@
\<^plugin> argument: cartouche
\<^print>
\<^prop> argument: cartouche
+\<^scala> argument: cartouche
+\<^scala_function> argument: cartouche
\<^session> argument: cartouche
\<^simproc> argument: cartouche
\<^sort> argument: cartouche
--- a/lib/Tools/scala Sun May 24 09:04:25 2020 +0200
+++ b/lib/Tools/scala Sun May 24 21:11:23 2020 +0200
@@ -13,5 +13,9 @@
SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
done
+[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+unset CLASSPATH
+
isabelle_scala scala "${SCALA_ARGS[@]}" \
- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" \
+ -Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/texinputs/isabellesym.sty Sun May 24 09:04:25 2020 +0200
+++ b/lib/texinputs/isabellesym.sty Sun May 24 21:11:23 2020 +0200
@@ -402,6 +402,8 @@
\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
+\newcommand{\isactrlscala}{\isakeywordcontrol{scala}}
+\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}}
\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
--- a/src/Pure/Concurrent/future.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Concurrent/future.ML Sun May 24 21:11:23 2020 +0200
@@ -276,11 +276,9 @@
fun worker_start name = (*requires SYNCHRONIZED*)
let
- val threads_stack_limit =
- Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
- val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
val worker =
- Isabelle_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+ Isabelle_Thread.fork
+ {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
(fn () => worker_loop name);
in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
--- a/src/Pure/Concurrent/isabelle_thread.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Sun May 24 21:11:23 2020 +0200
@@ -8,6 +8,7 @@
sig
val is_self: Thread.thread -> bool
val get_name: unit -> string
+ val stack_limit: unit -> int option
type params = {name: string, stack_limit: int option, interrupts: bool}
val attributes: params -> Thread.threadAttribute list
val fork: params -> (unit -> unit) -> Thread.thread
@@ -43,6 +44,12 @@
(* fork *)
+fun stack_limit () =
+ let
+ val threads_stack_limit =
+ Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
+ in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;
+
type params = {name: string, stack_limit: int option, interrupts: bool};
fun attributes ({stack_limit, interrupts, ...}: params) =
--- a/src/Pure/General/word.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/General/word.scala Sun May 24 21:11:23 2020 +0200
@@ -77,11 +77,11 @@
explode(_ == sep, text)
def explode(text: String): List[String] =
- explode(Character.isWhitespace(_), text)
+ explode(Character.isWhitespace _, text)
/* brackets */
- val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
- val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
+ val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"
+ val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"
}
--- a/src/Pure/ML/ml_process.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/ML/ml_process.scala Sun May 24 21:11:23 2020 +0200
@@ -92,8 +92,9 @@
ML_Syntax.print_list(
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
- List("Resources.init_session_base" +
- " {session_positions = " + print_sessions(sessions_structure.session_positions) +
+ List("Resources.init_session" +
+ "{pide = false" +
+ ", session_positions = " + print_sessions(sessions_structure.session_positions) +
", session_directories = " + print_table(sessions_structure.dest_session_directories) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
@@ -112,6 +113,8 @@
val isabelle_tmp = Isabelle_System.tmp_dir("process")
val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
+ val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
+
val ml_runtime_options =
{
val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
@@ -134,7 +137,7 @@
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
Bash.strings(bash_args),
cwd = cwd,
- env = env ++ env_options ++ env_tmp,
+ env = env ++ env_options ++ env_tmp ++ env_functions,
redirect = redirect,
cleanup = () =>
{
--- a/src/Pure/PIDE/markup.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/markup.ML Sun May 24 21:11:23 2020 +0200
@@ -68,6 +68,7 @@
val export_pathN: string val export_path: string -> T
val urlN: string val url: string -> T
val docN: string val doc: string -> T
+ val scala_functionN: string val scala_function: string -> T
val markupN: string
val consistentN: string
val unbreakableN: string
@@ -405,6 +406,7 @@
val (export_pathN, export_path) = markup_string "export_path" nameN;
val (urlN, url) = markup_string "url" nameN;
val (docN, doc) = markup_string "doc" nameN;
+val (scala_functionN, scala_function) = markup_string "scala_function" nameN;
(* pretty printing *)
--- a/src/Pure/PIDE/protocol.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML Sun May 24 21:11:23 2020 +0200
@@ -12,13 +12,17 @@
(fn args => List.app writeln args);
val _ =
+ Isabelle_Process.protocol_command "Prover.stop"
+ (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc));
+
+val _ =
Isabelle_Process.protocol_command "Prover.options"
(fn [options_yxml] =>
(Options.set_default (Options.decode (YXML.parse_body options_yxml));
Isabelle_Process.init_options_interactive ()));
val _ =
- Isabelle_Process.protocol_command "Prover.init_session_base"
+ Isabelle_Process.protocol_command "Prover.init_session"
(fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
loaded_theories_yxml] =>
let
@@ -27,8 +31,9 @@
val decode_sessions =
YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
in
- Resources.init_session_base
- {session_positions = decode_sessions session_positions_yxml,
+ Resources.init_session
+ {pide = true,
+ session_positions = decode_sessions session_positions_yxml,
session_directories = decode_table session_directories_yxml,
docs = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
--- a/src/Pure/PIDE/protocol.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala Sun May 24 21:11:23 2020 +0200
@@ -328,9 +328,9 @@
Symbol.encode_yxml(list(pair(string, properties))(lst))
}
- def session_base(resources: Resources)
+ def init_session(resources: Resources)
{
- protocol_command("Prover.init_session_base",
+ protocol_command("Prover.init_session",
encode_sessions(resources.sessions_structure.session_positions),
encode_table(resources.sessions_structure.dest_session_directories),
encode_list(resources.session_base.doc_names),
--- a/src/Pure/PIDE/resources.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/resources.ML Sun May 24 21:11:23 2020 +0200
@@ -7,13 +7,15 @@
signature RESOURCES =
sig
val default_qualifier: string
- val init_session_base:
- {session_positions: (string * Properties.T) list,
+ val init_session:
+ {pide: bool,
+ session_positions: (string * Properties.T) list,
session_directories: (string * string) list,
docs: string list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
val finish_session_base: unit -> unit
+ val is_pide: unit -> bool
val global_theory: string -> string option
val loaded_theory: string -> bool
val check_session: Proof.context -> string * Position.T -> string
@@ -52,7 +54,8 @@
{pos = Position.of_properties props, serial = serial ()};
val empty_session_base =
- {session_positions = []: (string * entry) list,
+ {pide = false,
+ session_positions = []: (string * entry) list,
session_directories = Symtab.empty: Path.T list Symtab.table,
docs = []: (string * entry) list,
global_theories = Symtab.empty: string Symtab.table,
@@ -61,11 +64,12 @@
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
-fun init_session_base
- {session_positions, session_directories, docs, global_theories, loaded_theories} =
+fun init_session
+ {pide, session_positions, session_directories, docs, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
- {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+ {pide = pide,
+ session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
session_directories =
fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
session_directories Symtab.empty,
@@ -76,7 +80,8 @@
fun finish_session_base () =
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
- {session_positions = [],
+ {pide = false,
+ session_positions = [],
session_directories = Symtab.empty,
docs = [],
global_theories = global_theories,
@@ -84,6 +89,8 @@
fun get_session_base f = f (Synchronized.value global_session_base);
+fun is_pide () = get_session_base #pide;
+
fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
--- a/src/Pure/PIDE/session.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/session.scala Sun May 24 21:11:23 2020 +0200
@@ -548,7 +548,7 @@
case _ if output.is_init =>
prover.get.options(file_formats.prover_options(session_options))
- prover.get.session_base(resources)
+ prover.get.init_session(resources)
phase = Session.Ready
debugger.ready()
--- a/src/Pure/ROOT.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/ROOT.ML Sun May 24 21:11:23 2020 +0200
@@ -328,6 +328,7 @@
ML_file "System/message_channel.ML";
ML_file "System/isabelle_process.ML";
ML_file "System/scala.ML";
+ML_file "System/scala_check.ML";
ML_file "Thy/bibtex.ML";
ML_file "PIDE/protocol.ML";
ML_file "General/output_primitives_virtual.ML";
--- a/src/Pure/System/isabelle_process.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML Sun May 24 21:11:23 2020 +0200
@@ -7,8 +7,7 @@
signature ISABELLE_PROCESS =
sig
val is_active: unit -> bool
- exception STOP
- exception EXIT of int
+ exception STOP of int
val protocol_command: string -> (string list -> unit) -> unit
val reset_tracing: Document_ID.exec -> unit
val crashes: exn list Synchronized.var
@@ -36,10 +35,9 @@
(* protocol commands *)
-exception STOP;
-exception EXIT of int;
+exception STOP of int;
-val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
+val is_protocol_exn = fn STOP _ => true | _ => false;
local
@@ -191,7 +189,7 @@
let
val _ =
(case Byte_Message.read_message in_stream of
- NONE => raise STOP
+ NONE => raise STOP 0
| SOME [] => Output.system_message "Isabelle process: no input"
| SOME (name :: args) => run_command name args)
handle exn =>
@@ -217,8 +215,7 @@
in
(case result of
- Exn.Exn STOP => ()
- | Exn.Exn (EXIT rc) => exit rc
+ Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
| _ => Exn.release result)
end);
--- a/src/Pure/System/isabelle_system.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala Sun May 24 21:11:23 2020 +0200
@@ -63,95 +63,98 @@
_services.get
}
- def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
+ def init(isabelle_root: String = "", cygwin_root: String = "")
{
- if (_settings.isEmpty || _services.isEmpty) {
- val isabelle_root1 =
- bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
+ synchronized {
+ if (_settings.isEmpty || _services.isEmpty) {
+ val isabelle_root1 =
+ bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
- val cygwin_root1 =
- if (Platform.is_windows)
- bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
- else ""
+ val cygwin_root1 =
+ if (Platform.is_windows)
+ bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
+ else ""
- if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
+ if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
- def set_cygwin_root()
- {
- if (Platform.is_windows)
- _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
- }
+ def set_cygwin_root()
+ {
+ if (Platform.is_windows)
+ _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
+ }
- set_cygwin_root()
+ set_cygwin_root()
- def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
- if (env.isDefinedAt(entry._1) || entry._2 == "") env
- else env + entry
+ def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
+ if (env.isDefinedAt(entry._1) || entry._2 == "") env
+ else env + entry
- val env =
- {
- val temp_windows =
+ val env =
{
- val temp = if (Platform.is_windows) System.getenv("TEMP") else null
- if (temp != null && temp.contains('\\')) temp else ""
+ val temp_windows =
+ {
+ val temp = if (Platform.is_windows) System.getenv("TEMP") else null
+ if (temp != null && temp.contains('\\')) temp else ""
+ }
+ val user_home = System.getProperty("user.home", "")
+ val isabelle_app = System.getProperty("isabelle.app", "")
+
+ default(
+ default(
+ default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
+ "TEMP_WINDOWS" -> temp_windows),
+ "HOME" -> user_home),
+ "ISABELLE_APP" -> "true")
}
- val user_home = System.getProperty("user.home", "")
- val isabelle_app = System.getProperty("isabelle.app", "")
-
- default(
- default(
- default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
- "TEMP_WINDOWS" -> temp_windows),
- "HOME" -> user_home),
- "ISABELLE_APP" -> "true")
- }
- val settings =
- {
- val dump = JFile.createTempFile("settings", null)
- dump.deleteOnExit
- try {
- val cmd1 =
- if (Platform.is_windows)
- List(cygwin_root1 + "\\bin\\bash", "-l",
- File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
- else
- List(isabelle_root1 + "/bin/isabelle")
- val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
+ val settings =
+ {
+ val dump = JFile.createTempFile("settings", null)
+ dump.deleteOnExit
+ try {
+ val cmd1 =
+ if (Platform.is_windows)
+ List(cygwin_root1 + "\\bin\\bash", "-l",
+ File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
+ else
+ List(isabelle_root1 + "/bin/isabelle")
+ val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
- val (output, rc) = process_output(process(cmd, env = env, redirect = true))
- if (rc != 0) error(output)
+ val (output, rc) = process_output(process(cmd, env = env, redirect = true))
+ if (rc != 0) error(output)
- val entries =
- (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
- val i = entry.indexOf('=')
- if (i <= 0) entry -> ""
- else entry.substring(0, i) -> entry.substring(i + 1)
- }).toMap
- entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
+ val entries =
+ (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
+ val i = entry.indexOf('=')
+ if (i <= 0) entry -> ""
+ else entry.substring(0, i) -> entry.substring(i + 1)
+ }).toMap
+ entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
+ }
+ finally { dump.delete }
}
- finally { dump.delete }
- }
- _settings = Some(settings)
- set_cygwin_root()
+ _settings = Some(settings)
+ set_cygwin_root()
- val variable = "ISABELLE_SCALA_SERVICES"
- val services =
- for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
- yield {
- def err(msg: String): Nothing =
- error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
- try {
- Class.forName(name).asInstanceOf[Class[Service]]
- .getDeclaredConstructor().newInstance()
+ val variable = "ISABELLE_SCALA_SERVICES"
+ val services =
+ for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
+ yield {
+ def err(msg: String): Nothing =
+ error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+ try {
+ Class.forName(name).asInstanceOf[Class[Service]]
+ .getDeclaredConstructor().newInstance()
+ }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
}
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- _services = Some(services)
+ _services = Some(services)
+ }
}
+ Scala.Compiler.default_context
}
--- a/src/Pure/System/scala.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/scala.ML Sun May 24 21:11:23 2020 +0200
@@ -6,15 +6,17 @@
signature SCALA =
sig
- val method: string -> string -> string
- val promise_method: string -> string -> string future
+ val functions: unit -> string list
+ val check_function: Proof.context -> string * Position.T -> string
+ val promise_function: string -> string -> string future
+ val function: string -> string -> string
exception Null
end;
structure Scala: SCALA =
struct
-(** invoke JVM method via Isabelle/Scala **)
+(** invoke Scala functions from ML **)
val _ = Session.protocol_handler "isabelle.Scala";
@@ -27,10 +29,11 @@
Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
-(* method invocation *)
+(* invoke function *)
-fun promise_method name arg =
+fun promise_function name arg =
let
+ val _ = if Resources.is_pide () then () else raise Fail "PIDE session required";
val id = new_id ();
fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
val promise = Future.promise_name "invoke_scala" abort : string future;
@@ -38,7 +41,7 @@
val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
in promise end;
-fun method name arg = Future.join (promise_method name arg);
+fun function name arg = Future.join (promise_function name arg);
(* fulfill *)
@@ -67,4 +70,38 @@
fulfill id tag res
handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
+
+(* registered functions *)
+
+fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
+
+fun check_function ctxt (name, pos) =
+ let
+ val kind = Markup.scala_functionN;
+ val funs = functions ();
+ in
+ if member (op =) funs name then
+ (Context_Position.report ctxt pos (Markup.scala_function name); name)
+ else
+ let
+ val completion_report =
+ Completion.make_report (name, pos)
+ (fn completed =>
+ filter completed funs
+ |> sort_strings
+ |> map (fn a => (a, (kind, a))));
+ in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
+ end;
+
+val _ = Theory.setup
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
+ (Scan.lift Parse.embedded_position) check_function #>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
+ (Args.context -- Scan.lift Parse.embedded_position
+ >> (uncurry check_function #> ML_Syntax.print_string)) #>
+ ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+ let val name = check_function ctxt arg
+ in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
+
end;
--- a/src/Pure/System/scala.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/scala.scala Sun May 24 21:11:23 2020 +0200
@@ -7,87 +7,123 @@
package isabelle
-import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-import java.io.{File => JFile}
+import java.io.{File => JFile, StringWriter, PrintWriter}
-import scala.util.matching.Regex
-import scala.tools.nsc.GenericRunnerSettings
+import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
+import scala.tools.nsc.interpreter.IMain
object Scala
{
- /* compiler classpath and settings */
+ /** compiler **/
- def compiler_classpath(jar_dirs: List[JFile]): String =
+ object Compiler
{
- def find_jars(dir: JFile): List[String] =
- File.find_files(dir, file => file.getName.endsWith(".jar")).
- map(File.absolute_name)
+ lazy val default_context: Context = context()
+
+ def context(
+ error: String => Unit = Exn.error,
+ jar_dirs: List[JFile] = Nil): Context =
+ {
+ def find_jars(dir: JFile): List[String] =
+ File.find_files(dir, file => file.getName.endsWith(".jar")).
+ map(File.absolute_name)
+
+ val class_path =
+ for {
+ prop <- List("isabelle.scala.classpath", "java.class.path")
+ path = System.getProperty(prop, "") if path != "\"\""
+ elem <- space_explode(JFile.pathSeparatorChar, path)
+ } yield elem
+
+ val settings = new GenericRunnerSettings(error)
+ settings.classpath.value =
+ (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+
+ new Context(settings)
+ }
+
+ def default_print_writer: PrintWriter =
+ new NewLinePrintWriter(new ConsoleWriter, true)
+
+ class Context private [Compiler](val settings: GenericRunnerSettings)
+ {
+ override def toString: String = settings.toString
- val class_path =
- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+ def interpreter(
+ print_writer: PrintWriter = default_print_writer,
+ class_loader: ClassLoader = null): IMain =
+ {
+ new IMain(settings, print_writer)
+ {
+ override def parentClassLoader: ClassLoader =
+ if (class_loader == null) super.parentClassLoader
+ else class_loader
+ }
+ }
- (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+ def toplevel(source: String): List[String] =
+ {
+ val out = new StringWriter
+ val interp = interpreter(new PrintWriter(out))
+ val rep = new interp.ReadEvalPrint
+ val ok = interp.withLabel("\u0001") { rep.compile(source) }
+ out.close
+
+ val Error = """(?s)^\S* error: (.*)$""".r
+ val errors =
+ space_explode('\u0001', Library.strip_ansi_color(out.toString)).
+ collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
+
+ if (!ok && errors.isEmpty) List("Error") else errors
+ }
+
+ def check(body: String): List[String] =
+ {
+ try { toplevel("package test\nobject Test { " + body + " }") }
+ catch { case ERROR(msg) => List(msg) }
+ }
+ }
}
- def compiler_settings(
- error: String => Unit = Exn.error,
- jar_dirs: List[JFile] = Nil): GenericRunnerSettings =
+ def check_yxml(body: String): String =
{
- val settings = new GenericRunnerSettings(error)
- settings.classpath.value = compiler_classpath(jar_dirs)
- settings
+ val errors = Compiler.default_context.check(body)
+ locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
- /** invoke JVM method via Isabelle/Scala **/
+ /** invoke Scala functions from ML **/
- /* method reflection */
-
- private val Ext = new Regex("(.*)\\.([^.]*)")
- private val STRING = Class.forName("java.lang.String")
+ /* registered functions */
- private def get_method(name: String): String => String =
- name match {
- case Ext(class_name, method_name) =>
- val m =
- try { Class.forName(class_name).getMethod(method_name, STRING) }
- catch {
- case _: ClassNotFoundException | _: NoSuchMethodException =>
- error("No such method: " + quote(name))
- }
- if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
- if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
+ sealed case class Fun(name: String, apply: String => String)
+ {
+ override def toString: String = name
+ }
- (arg: String) => {
- try { m.invoke(null, arg).asInstanceOf[String] }
- catch {
- case e: InvocationTargetException if e.getCause != null =>
- throw e.getCause
- }
- }
- case _ => error("Malformed method name: " + quote(name))
- }
+ lazy val functions: List[Fun] =
+ Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
- /* method invocation */
+ /* invoke function */
object Tag extends Enumeration
{
val NULL, OK, ERROR, FAIL, INTERRUPT = Value
}
- def method(name: String, arg: String): (Tag.Value, String) =
- Exn.capture { get_method(name) } match {
- case Exn.Res(f) =>
- Exn.capture { f(arg) } match {
+ def function(name: String, arg: String): (Tag.Value, String) =
+ functions.find(fun => fun.name == name) match {
+ case Some(fun) =>
+ Exn.capture { fun.apply(arg) } match {
case Exn.Res(null) => (Tag.NULL, "")
case Exn.Res(res) => (Tag.OK, res)
case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
}
- case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
+ case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
}
}
@@ -129,7 +165,7 @@
case Markup.Invoke_Scala(name, id) =>
futures += (id ->
Future.fork {
- val (tag, result) = Scala.method(name, msg.text)
+ val (tag, result) = Scala.function(name, msg.text)
fulfill(id, tag, result)
})
true
@@ -155,3 +191,13 @@
Markup.Invoke_Scala.name -> invoke_scala,
Markup.Cancel_Scala.name -> cancel_scala)
}
+
+
+/* registered functions */
+
+class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service
+
+class Functions extends Isabelle_Scala_Functions(
+ Scala.Fun("echo", identity),
+ Scala.Fun("scala_check", Scala.check_yxml),
+ Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala_check.ML Sun May 24 21:11:23 2020 +0200
@@ -0,0 +1,22 @@
+(* Title: Pure/System/scala_check.ML
+ Author: Makarius
+
+Semantic check of Scala sources.
+*)
+
+signature SCALA_CHECK =
+sig
+ val decl: string -> unit
+end;
+
+structure Scala_Check: SCALA_CHECK =
+struct
+
+fun decl source =
+ let val errors =
+ \<^scala>\<open>scala_check\<close> source
+ |> YXML.parse_body
+ |> let open XML.Decode in list string end
+ in if null errors then () else error (cat_lines errors) end;
+
+end;
--- a/src/Pure/Thy/bibtex.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML Sun May 24 21:11:23 2020 +0200
@@ -20,7 +20,7 @@
type message = string * Position.T;
fun check_database pos0 database =
- Scala.method "isabelle.Bibtex.check_database_yxml" database
+ \<^scala>\<open>check_bibtex_database\<close> database
|> YXML.parse_body
|> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
|> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
--- a/src/Pure/Tools/build.ML Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Tools/build.ML Sun May 24 21:11:23 2020 +0200
@@ -132,7 +132,8 @@
(* build session *)
datatype args = Args of
- {symbol_codes: (string * int) list,
+ {pide: bool,
+ symbol_codes: (string * int) list,
command_timings: Properties.T list,
verbose: bool,
browser_info: Path.T,
@@ -150,7 +151,7 @@
loaded_theories: string list,
bibtex_entries: string list};
-fun decode_args yxml =
+fun decode_args pide yxml =
let
open XML.Decode;
val position = Position.of_properties o properties;
@@ -167,7 +168,7 @@
(pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
(YXML.parse_body yxml);
in
- Args {symbol_codes = symbol_codes, command_timings = command_timings,
+ Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings,
verbose = verbose, browser_info = Path.explode browser_info,
document_files = map (apply2 Path.explode) document_files,
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
@@ -177,15 +178,16 @@
bibtex_entries = bibtex_entries}
end;
-fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files,
+fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files,
graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions,
session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
let
val symbols = HTML.make_symbols symbol_codes;
val _ =
- Resources.init_session_base
- {session_positions = session_positions,
+ Resources.init_session
+ {pide = pide,
+ session_positions = session_positions,
session_directories = session_directories,
docs = doc_names,
global_theories = global_theories,
@@ -233,7 +235,7 @@
val _ = SHA1.test_samples ();
val _ = Options.load_default ();
val _ = Isabelle_Process.init_options ();
- val args = decode_args (File.read (Path.explode args_file));
+ val args = decode_args false (File.read (Path.explode args_file));
val _ =
Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
build_session args
@@ -245,25 +247,24 @@
(* PIDE version *)
-fun build_session_finished errs =
- XML.Encode.list XML.Encode.string errs
- |> Output.protocol_message Markup.build_session_finished;
-
val _ =
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
let
- val args = decode_args args_yxml;
- val errs =
- Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
- (Runtime.exn_message_list exn handle _ (*sic!*) =>
- (build_session_finished ["CRASHED"];
- raise Isabelle_Process.EXIT 2));
- val _ = build_session_finished errs;
+ val args = decode_args true args_yxml;
+ fun exec e =
+ if can Theory.get_pure () then
+ Isabelle_Thread.fork
+ {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
+ interrupts = false} e
+ |> ignore
+ else e ();
in
- if null errs
- then raise Isabelle_Process.STOP
- else raise Isabelle_Process.EXIT 1
+ exec (fn () =>
+ (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
+ ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
+ |> let open XML.Encode in pair int (list string) end
+ |> Output.protocol_message Markup.build_session_finished)
end
| _ => raise Match);
--- a/src/Pure/Tools/build.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Tools/build.scala Sun May 24 21:11:23 2020 +0200
@@ -216,7 +216,7 @@
}
else Nil
- if (options.bool("pide_build")) {
+ if (options.bool("pide_session")) {
val resources = new Resources(sessions_structure, deps(parent))
val session = new Session(options, resources)
@@ -234,15 +234,23 @@
private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
{
- val errors =
+ val (rc, errors) =
try {
- for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)))
- yield {
- val prt = Protocol_Message.expose_no_reports(err)
- Pretty.string_of(prt, metric = Symbol.Metric)
+ val (rc, errs) =
+ {
+ import XML.Decode._
+ pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
}
+ val errors =
+ for (err <- errs) yield {
+ val prt = Protocol_Message.expose_no_reports(err)
+ Pretty.string_of(prt, metric = Symbol.Metric)
+ }
+ (rc, errors)
}
- catch { case ERROR(err) => List(err) }
+ catch { case ERROR(err) => (2, List(err)) }
+
+ session.protocol_command("Prover.stop", rc.toString)
build_session_errors.fulfill(errors)
true
}
--- a/src/Pure/library.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/library.scala Sun May 24 21:11:23 2020 +0200
@@ -144,6 +144,9 @@
def isolate_substring(s: String): String = new String(s.toCharArray)
+ def strip_ansi_color(s: String): String =
+ s.replaceAll("""\u001b\[\d+m""", "")
+
/* quote */
--- a/src/Tools/jEdit/src/jedit_lib.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun May 24 21:11:23 2020 +0200
@@ -25,6 +25,12 @@
object JEdit_Lib
{
+ /* jEdit directories */
+
+ def directories: List[JFile] =
+ (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
+
+
/* location within multi-screen environment */
final case class Screen_Location(point: Point, bounds: Rectangle)
--- a/src/Tools/jEdit/src/scala_console.scala Sun May 24 09:04:25 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Sun May 24 21:11:23 2020 +0200
@@ -10,26 +10,12 @@
import isabelle._
import console.{Console, ConsolePane, Shell, Output}
-
-import org.gjt.sp.jedit.{jEdit, JARClassLoader}
-import org.gjt.sp.jedit.MiscUtilities
-
-import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
-
-import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
-import scala.tools.nsc.interpreter.IMain
-import scala.collection.mutable
+import org.gjt.sp.jedit.JARClassLoader
+import java.io.{OutputStream, Writer, PrintWriter}
class Scala_Console extends Shell("Scala")
{
- /* reconstructed jEdit/plugin classpath */
-
- private def jar_dirs: List[JFile] =
- (proper_string(jEdit.getSettingsDirectory).toList :::
- proper_string(jEdit.getJEditHome).toList).map(new JFile(_))
-
-
/* global state -- owned by GUI thread */
@volatile private var interpreters = Map.empty[Console, Interpreter]
@@ -113,12 +99,11 @@
private val running = Synchronized[Option[Thread]](None)
def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
- private val settings = Scala.compiler_settings(error = report_error, jar_dirs = jar_dirs)
-
- private val interp = new IMain(settings, new PrintWriter(console_writer, true))
- {
- override def parentClassLoader = new JARClassLoader
- }
+ private val interp =
+ Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
+ interpreter(
+ print_writer = new PrintWriter(console_writer, true),
+ class_loader = new JARClassLoader)
val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
{