# HG changeset patch
# User wenzelm
# Date 1571494584 -7200
# Node ID 3ed399935d7c602dba239e258b23b1ddc5d3dda5
# Parent  c550368a4e2987469b3ea450dd485c3e42facc66# Parent  9e05f382e749f60cf48547a06b6a408b47bd6bf1
merged

diff -r c550368a4e29 -r 3ed399935d7c src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/General/output.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -29,6 +29,7 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
+  val protocol_message_undefined: Properties.T -> string list -> unit
   val writelns: string list -> unit
   val state: string -> unit
   val information: string -> unit
@@ -120,6 +121,9 @@
 
 exception Protocol_Message of Properties.T;
 
+fun protocol_message_undefined props (_: string list) =
+  raise Protocol_Message props;
+
 fun init_channels () =
  (writeln_fn := (physical_writeln o implode);
   state_fn := (fn ss => ! writeln_fn ss);
@@ -132,7 +136,7 @@
   status_fn := Output_Primitives.ignore_outputs;
   report_fn := Output_Primitives.ignore_outputs;
   result_fn := (fn _ => Output_Primitives.ignore_outputs);
-  protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
+  protocol_message_fn := protocol_message_undefined);
 
 val _ = if Thread_Data.is_virtual then () else init_channels ();
 
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/PIDE/protocol_message.ML
--- a/src/Pure/PIDE/protocol_message.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/PIDE/protocol_message.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -6,6 +6,7 @@
 
 signature PROTOCOL_MESSAGE =
 sig
+  val inline: string -> Properties.T -> unit
   val command_positions: string -> XML.body -> XML.body
   val command_positions_yxml: string -> string -> string
 end;
@@ -13,6 +14,10 @@
 structure Protocol_Message: PROTOCOL_MESSAGE =
 struct
 
+fun inline a args =
+  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
+
+
 fun command_positions id =
   let
     fun attribute (a, b) =
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/ROOT	Sat Oct 19 16:16:24 2019 +0200
@@ -4,8 +4,9 @@
   description "
     The Pure logical framework.
   "
-  options [threads = 1, export_theory, export_proofs]
+  options [threads = 1, export_proofs]
+  theories [export_theory]
+    Pure (global)
   theories
-    Pure (global)
     ML_Bootstrap (global)
     Sessions
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/ROOT.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -90,6 +90,7 @@
 
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/yxml.ML";
+ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 
 ML_file "General/change_table.ML";
@@ -314,7 +315,6 @@
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
-ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document.ML";
 
 (*theory and proof operations*)
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/Thy/export.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -16,6 +16,7 @@
   val export_executable_file: theory -> Path.binding -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
+  val protocol_message: Properties.T -> string list -> unit
 end;
 
 structure Export: EXPORT =
@@ -67,4 +68,24 @@
 fun message thy path =
   "See " ^ Markup.markup (markup thy path) "theory exports";
 
+
+(* protocol message (bootstrap) *)
+
+fun protocol_message props output =
+  (case props of
+    function :: args =>
+      if function = (Markup.functionN, Markup.exportN) andalso
+        not (null args) andalso #1 (hd args) = Markup.idN
+      then
+        let
+          val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
+          val _ = File.write_list path output;
+        in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
+      else raise Output.Protocol_Message props
+  | [] => raise Output.Protocol_Message props);
+
+val _ =
+  if Thread_Data.is_virtual then ()
+  else Private_Output.protocol_message_fn := protocol_message;
+
 end;
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/Thy/export_theory.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -259,17 +259,18 @@
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
-    fun encode_thm serial raw_thm =
+    fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
-        val boxes =
-          raw_thm |> Thm_Deps.proof_boxes (fn thm_id =>
-            if #serial thm_id = serial then false else is_some (lookup_thm_id thm_id));
-
-        val thm = clean_thm raw_thm;
+        val thm = Thm.unconstrainT (clean_thm raw_thm);
+        val dep_boxes =
+          thm |> Thm_Deps.proof_boxes (fn thm_id' =>
+            if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
+        val boxes = dep_boxes @ [thm_id];
         val (prop, SOME proof) =
           SOME (if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof)
           |> standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
+        val _ = Proofterm.commit_proof proof;
       in
         (prop, (deps, (boxes, proof))) |>
           let
@@ -279,10 +280,10 @@
           in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
       end;
 
-    fun buffer_export_thm (serial, thm_name) =
+    fun buffer_export_thm (thm_id, thm_name) =
       let
-        val markup = entity_markup_thm (serial, thm_name);
-        val body = encode_thm serial (Global_Theory.get_thm_name thy (thm_name, Position.none));
+        val markup = entity_markup_thm (#serial thm_id, thm_name);
+        val body = encode_thm thm_id (Global_Theory.get_thm_name thy (thm_name, Position.none));
       in YXML.buffer (XML.Elem (markup, body)) end;
 
     val _ =
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/Tools/build.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -69,14 +69,11 @@
 
 (* protocol messages *)
 
-fun inline_message a args =
-  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
-
 fun protocol_message props output =
   (case props of
     function :: args =>
       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
-        inline_message (#2 function) args
+        Protocol_Message.inline (#2 function) args
       else if function = Markup.command_timing then
         let
           val name = the_default "" (Properties.get args Markup.nameN);
@@ -88,23 +85,17 @@
         in
           if is_significant then
             (case approximative_id name pos of
-              SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
+              SOME id =>
+                Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed)
             | NONE => ())
           else ()
         end
       else if function = Markup.theory_timing then
-        inline_message (#2 function) args
-      else if function = (Markup.functionN, Markup.exportN) andalso
-        not (null args) andalso #1 (hd args) = Markup.idN
-      then
-        let
-          val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
-          val _ = File.write_list path output;
-        in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
+        Protocol_Message.inline (#2 function) args
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
-        | NONE => raise Output.Protocol_Message props)
+        | NONE => Export.protocol_message props output)
   | [] => raise Output.Protocol_Message props);
 
 
@@ -240,6 +231,7 @@
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
         build_session args
       handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
+    val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined;
     val _ = Options.reset_default ();
   in () end;
 
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/global_theory.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -13,7 +13,7 @@
   val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
   val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
-  val dest_thm_names: theory -> (serial * Thm_Name.T) list
+  val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
   val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
   val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
   val get_thms: theory -> xstring -> thm list
@@ -112,7 +112,12 @@
     NONE => Lazy.lazy (fn () => make_thm_names thy)
   | SOME lazy_tab => lazy_tab);
 
-val dest_thm_names = Inttab.dest o Lazy.force o get_thm_names;
+fun dest_thm_names thy =
+  let
+    val theory_name = Context.theory_long_name thy;
+    fun thm_id i = Proofterm.make_thm_id (i, theory_name);
+    val thm_names = Lazy.force (get_thm_names thy);
+  in Inttab.fold_rev (fn (i, thm_name) => cons (thm_id i, thm_name)) thm_names [] end;
 
 fun lookup_thm_id thy =
   let
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/proofterm.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -136,7 +136,7 @@
   val equal_intr_proof: term -> term -> proof -> proof -> proof
   val equal_elim_proof: term -> term -> proof -> proof -> proof
   val abstract_rule_proof: string * term -> proof -> proof
-  val combination_proof: typ -> term -> term -> term -> term -> proof -> proof -> proof
+  val combination_proof: term -> term -> term -> term -> proof -> proof -> proof
   val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     sort list -> proof -> proof
   val of_sort_proof: Sorts.algebra ->
@@ -171,6 +171,7 @@
 
   val export_enabled: unit -> bool
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+  val commit_proof: proof -> unit
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
     term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
@@ -1313,7 +1314,7 @@
   | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
   | check_comb _ = false;
 
-fun combination_proof A f g t u prf1 prf2 =
+fun combination_proof f g t u prf1 prf2 =
   let
     val f = Envir.beta_norm f;
     val g = Envir.beta_norm g;
@@ -2117,6 +2118,24 @@
 
 fun export_enabled () = Options.default_bool "export_proofs";
 
+fun commit_proof proof =
+  let
+    fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
+      | export_boxes (Abst (_, _, prf)) = export_boxes prf
+      | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
+      | export_boxes (prf % _) = export_boxes prf
+      | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
+          (fn boxes =>
+            if Inttab.defined boxes i then boxes
+            else
+              let
+                val prf = thm_body_proof_raw thm_body;
+                val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
+              in export_boxes prf boxes' end)
+      | export_boxes _ = I;
+    val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
+  in List.app (Lazy.force o #2) boxes end;
+
 local
 
 fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
@@ -2162,28 +2181,10 @@
       strict = false}
   end;
 
-fun force_export_boxes proof =
-  let
-    fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
-      | export_boxes (Abst (_, _, prf)) = export_boxes prf
-      | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
-      | export_boxes (prf % _) = export_boxes prf
-      | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
-          (fn boxes =>
-            if Inttab.defined boxes i then boxes
-            else
-              let
-                val prf = thm_body_proof_raw thm_body;
-                val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
-              in export_boxes prf boxes' end)
-      | export_boxes _ = I;
-    val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
-  in List.app (Lazy.force o #2) boxes end;
-
 fun export thy i prop prf =
   if export_enabled () then
     let
-      val _ = force_export_boxes prf;
+      val _ = commit_proof prf;
       val _ = export_proof thy i prop prf;
     in () end
   else ();
diff -r c550368a4e29 -r 3ed399935d7c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Oct 19 09:15:41 2019 +0000
+++ b/src/Pure/thm.ML	Sat Oct 19 16:16:24 2019 +0200
@@ -1377,7 +1377,7 @@
       (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
        Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
         (chktypes fT tT;
-          Thm (deriv_rule2 (Proofterm.combination_proof (domain_type fT) f g t u) der1 der2,
+          Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),