--- 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 ();
--- 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) =
--- 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
--- 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*)
--- 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;
--- 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 _ =
--- 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;
--- 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
--- 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 ();
--- 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),