src/Pure/Tools/build.ML
changeset 72103 7b318273a4aa
parent 72019 940195fbb282
child 72574 d892f6d66402
--- a/src/Pure/Tools/build.ML	Thu Aug 06 17:51:37 2020 +0200
+++ b/src/Pure/Tools/build.ML	Thu Aug 06 22:43:40 2020 +0200
@@ -4,12 +4,7 @@
 Build Isabelle sessions.
 *)
 
-signature BUILD =
-sig
-  val build: string -> unit
-end;
-
-structure Build: BUILD =
+structure Build: sig end =
 struct
 
 (* command timings *)
@@ -58,39 +53,6 @@
   in y end;
 
 
-(* protocol messages *)
-
-fun protocol_message props output =
-  (case props of
-    function :: args =>
-      if function = Markup.ML_statistics orelse function = Markup.task_statistics then
-        Protocol_Message.marker (#2 function) args
-      else if function = Markup.command_timing then
-        let
-          val name = the_default "" (Properties.get args Markup.nameN);
-          val pos = Position.of_properties args;
-          val {elapsed, ...} = Markup.parse_timing_properties args;
-          val is_significant =
-            Timing.is_relevant_time elapsed andalso
-            elapsed >= Options.default_seconds "command_timing_threshold";
-        in
-          if is_significant then
-            (case approximative_id name pos of
-              SOME id =>
-                Protocol_Message.marker (#2 function)
-                  (Markup.command_timing_properties id elapsed)
-            | NONE => ())
-          else ()
-        end
-      else if function = Markup.theory_timing orelse function = Markup.session_timing then
-        Protocol_Message.marker (#2 function) args
-      else
-        (case Markup.dest_loading_theory props of
-          SOME name => Protocol_Message.marker_text "loading_theory" name
-        | NONE => Export.protocol_message props output)
-  | [] => raise Output.Protocol_Message props);
-
-
 (* build theories *)
 
 fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
@@ -122,127 +84,72 @@
 
 (* build session *)
 
-datatype args = Args of
- {pide: bool,
-  symbol_codes: (string * int) list,
-  command_timings: Properties.T list,
-  verbose: bool,
-  browser_info: Path.T,
-  document_files: (Path.T * Path.T) list,
-  graph_file: Path.T,
-  parent_name: string,
-  chapter: string,
-  session_name: string,
-  master_dir: Path.T,
-  theories: (Options.T * (string * Position.T) list) list,
-  session_positions: (string * Properties.T) list,
-  session_directories: (string * string) list,
-  doc_names: string list,
-  global_theories: (string * string) list,
-  loaded_theories: string list,
-  bibtex_entries: string list};
-
-fun decode_args pide yxml =
-  let
-    open XML.Decode;
-    val position = Position.of_properties o properties;
-    val (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)))))))))))))))) =
-      pair (list (pair string int)) (pair (list properties) (pair bool (pair string
-        (pair (list (pair string string)) (pair string (pair string (pair string (pair string
-          (pair string
-            (pair (((list (pair Options.decode (list (pair string position))))))
-              (pair (list (pair string properties))
-                (pair (list (pair string string)) (pair (list string)
-                  (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
-      (YXML.parse_body yxml);
-  in
-    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,
-      session_name = session_name, master_dir = Path.explode master_dir, theories = theories,
-      session_positions = session_positions, session_directories = session_directories,
-      doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
-      bibtex_entries = bibtex_entries}
-  end;
-
-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
-        {pide = pide,
-         session_positions = session_positions,
-         session_directories = session_directories,
-         docs = doc_names,
-         global_theories = global_theories,
-         loaded_theories = loaded_theories};
-
-    val _ =
-      Session.init
-        symbols
-        (Options.default_bool "browser_info")
-        browser_info
-        (Options.default_string "document")
-        (Options.default_string "document_output")
-        (Present.document_variants (Options.default ()))
-        document_files
-        graph_file
-        parent_name
-        (chapter, session_name)
-        verbose;
-
-    val last_timing = get_timings (fold update_timings command_timings empty_timings);
-
-    val res1 =
-      theories |>
-        (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir)
-          |> session_timing
-          |> Exn.capture);
-    val res2 = Exn.capture Session.finish ();
-
-    val _ = Resources.finish_session_base ();
-    val _ = Par_Exn.release_all [res1, res2];
-    val _ =
-      if session_name = Context.PureN
-      then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
-  in () end;
-
-
-(* command-line tool *)
-
-fun inline_errors exn =
-  Runtime.exn_message_list exn
-  |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg));
-
-fun build args_file =
-  let
-    val _ = SHA1.test_samples ();
-    val _ = Options.load_default ();
-    val _ = Isabelle_Process.init_options ();
-    val args = decode_args false (File.read (Path.explode args_file));
-    val _ =
-      Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
-        build_session args
-      handle exn => (inline_errors exn; Exn.reraise exn);
-    val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined;
-    val _ = Options.reset_default ();
-  in () end;
-
-
-(* PIDE version *)
-
 val _ =
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
         let
-          val args = decode_args true args_yxml;
+          val (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)))))))))))))))) =
+            YXML.parse_body args_yxml |>
+              let
+                open XML.Decode;
+                val position = Position.of_properties o properties;
+                val path = Path.explode o string;
+              in
+                pair (list (pair string int)) (pair (list properties) (pair bool (pair path
+                  (pair (list (pair path path)) (pair path (pair string (pair string (pair string
+                    (pair path
+                      (pair (((list (pair Options.decode (list (pair string position))))))
+                        (pair (list (pair string properties))
+                          (pair (list (pair string string)) (pair (list string)
+                            (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
+              end;
+
+          val symbols = HTML.make_symbols symbol_codes;
+
+          fun build () =
+            let
+              val _ =
+                Resources.init_session
+                  {session_positions = session_positions,
+                   session_directories = session_directories,
+                   docs = doc_names,
+                   global_theories = global_theories,
+                   loaded_theories = loaded_theories};
+
+              val _ =
+                Session.init
+                  symbols
+                  (Options.default_bool "browser_info")
+                  browser_info
+                  (Options.default_string "document")
+                  (Options.default_string "document_output")
+                  (Present.document_variants (Options.default ()))
+                  document_files
+                  graph_file
+                  parent_name
+                  (chapter, session_name)
+                  verbose;
+
+              val last_timing = get_timings (fold update_timings command_timings empty_timings);
+
+              val res1 =
+                theories |>
+                  (List.app
+                      (build_theories symbols bibtex_entries last_timing session_name master_dir)
+                    |> session_timing
+                    |> Exn.capture);
+              val res2 = Exn.capture Session.finish ();
+
+              val _ = Resources.finish_session_base ();
+              val _ = Par_Exn.release_all [res1, res2];
+              val _ =
+                if session_name = Context.PureN
+                then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
+            in () end;
+
           fun exec e =
             if can Theory.get_pure () then
               Isabelle_Thread.fork
@@ -252,7 +159,7 @@
             else e ();
         in
           exec (fn () =>
-            (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
+            (Future.interruptible_task (fn () => (build (); (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)