--- a/src/Pure/ML/ml_process.scala Sun May 24 10:36:42 2020 +0200
+++ b/src/Pure/ML/ml_process.scala Sun May 24 12:38:41 2020 +0200
@@ -93,7 +93,8 @@
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
List("Resources.init_session" +
- " {session_positions = " + print_sessions(sessions_structure.session_positions) +
+ "{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) +
--- a/src/Pure/PIDE/protocol.ML Sun May 24 10:36:42 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML Sun May 24 12:38:41 2020 +0200
@@ -28,7 +28,8 @@
YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
in
Resources.init_session
- {session_positions = decode_sessions session_positions_yxml,
+ {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/resources.ML Sun May 24 10:36:42 2020 +0200
+++ b/src/Pure/PIDE/resources.ML Sun May 24 12:38:41 2020 +0200
@@ -8,12 +8,14 @@
sig
val default_qualifier: string
val init_session:
- {session_positions: (string * Properties.T) list,
+ {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,
@@ -62,10 +65,11 @@
Synchronized.var "Sessions.base" empty_session_base;
fun init_session
- {session_positions, session_directories, docs, global_theories, loaded_theories} =
+ {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/System/scala.ML Sun May 24 10:36:42 2020 +0200
+++ b/src/Pure/System/scala.ML Sun May 24 12:38:41 2020 +0200
@@ -32,6 +32,7 @@
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;
--- a/src/Pure/Tools/build.ML Sun May 24 10:36:42 2020 +0200
+++ b/src/Pure/Tools/build.ML Sun May 24 12:38:41 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,7 +178,7 @@
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
@@ -185,7 +186,8 @@
val _ =
Resources.init_session
- {session_positions = session_positions,
+ {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
@@ -253,7 +255,7 @@
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
let
- val args = decode_args args_yxml;
+ val args = decode_args true args_yxml;
val errs =
Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
(Runtime.exn_message_list exn handle _ (*sic!*) =>