# HG changeset patch
# User wenzelm
# Date 1590316721 -7200
# Node ID ad063ac1f6170dd4f5915d0af3b4cdf3b1e8b4a1
# Parent  aaa984499d361703cb2f3fb2470544e70396cd4d
more robust: explicit check for PIDE session;

diff -r aaa984499d36 -r ad063ac1f617 src/Pure/ML/ml_process.scala
--- 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) +
diff -r aaa984499d36 -r ad063ac1f617 src/Pure/PIDE/protocol.ML
--- 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,
diff -r aaa984499d36 -r ad063ac1f617 src/Pure/PIDE/resources.ML
--- 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;
 
diff -r aaa984499d36 -r ad063ac1f617 src/Pure/System/scala.ML
--- 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;
diff -r aaa984499d36 -r ad063ac1f617 src/Pure/Tools/build.ML
--- 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!*) =>