--- a/src/HOL/SPARK/Tools/spark_commands.ML Thu May 31 10:59:54 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Thu May 31 22:59:08 2018 +0200
@@ -92,13 +92,13 @@
end;
val _ =
- Outer_Syntax.command @{command_keyword spark_open_vcg}
+ Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>
"open a new SPARK environment and load a SPARK-generated .vcg file"
(Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
val _ =
- Outer_Syntax.command @{command_keyword spark_open}
+ Outer_Syntax.command \<^command_keyword>\<open>spark_open\<close>
"open a new SPARK environment and load a SPARK-generated .siv file"
(Resources.provide_parse_files "spark_open" -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
@@ -107,13 +107,13 @@
(Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
val _ =
- Outer_Syntax.command @{command_keyword spark_proof_functions}
+ Outer_Syntax.command \<^command_keyword>\<open>spark_proof_functions\<close>
"associate SPARK proof functions with terms"
(Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
(Toplevel.theory o fold add_proof_fun_cmd));
val _ =
- Outer_Syntax.command @{command_keyword spark_types}
+ Outer_Syntax.command \<^command_keyword>\<open>spark_types\<close>
"associate SPARK types with types"
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
Scan.optional (Args.parens (Parse.list1
@@ -121,12 +121,12 @@
(Toplevel.theory o fold add_spark_type_cmd));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
+ Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>spark_vc\<close>
"enter into proof mode for a specific verification condition"
(Parse.name >> prove_vc);
val _ =
- Outer_Syntax.command @{command_keyword spark_status}
+ Outer_Syntax.command \<^command_keyword>\<open>spark_status\<close>
"show the name and state of all loaded verification conditions"
(Scan.optional
(Args.parens
@@ -136,10 +136,10 @@
Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
val _ =
- Outer_Syntax.command @{command_keyword spark_end}
+ Outer_Syntax.command \<^command_keyword>\<open>spark_end\<close>
"close the current SPARK environment"
- (Scan.optional (@{keyword "("} |-- Parse.!!!
- (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
+ (Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!!
+ (Parse.reserved "incomplete" --| \<^keyword>\<open>)\<close>) >> K true) false >>
(Toplevel.theory o SPARK_VCs.close));
val _ = Theory.setup (Theory.at_end (fn thy =>
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu May 31 10:59:54 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu May 31 22:59:08 2018 +0200
@@ -101,7 +101,7 @@
val T = HOLogic.dest_setT setT;
val U = HOLogic.dest_setT (fastype_of u)
in
- Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) -->
+ Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
end;
@@ -150,7 +150,7 @@
in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
fun get_record_info thy T = (case Record.dest_recTs T of
- [(tyname, [@{typ unit}])] =>
+ [(tyname, [\<^typ>\<open>unit\<close>])] =>
Record.get_info thy (Long_Name.qualifier tyname)
| _ => NONE);
@@ -177,9 +177,9 @@
val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
val k = length cs;
val T = Type (tyname', []);
- val p = Const (@{const_name pos}, T --> HOLogic.intT);
- val v = Const (@{const_name val}, HOLogic.intT --> T);
- val card = Const (@{const_name card},
+ val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);
+ val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);
+ val card = Const (\<^const_name>\<open>card\<close>,
HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
fun mk_binrel_def s f = Logic.mk_equals
@@ -190,7 +190,7 @@
val (((def1, def2), def3), lthy) = thy |>
- Class.instantiation ([tyname'], [], @{sort spark_enum}) |>
+ Class.instantiation ([tyname'], [], \<^sort>\<open>spark_enum\<close>) |>
define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
(p,
@@ -199,9 +199,9 @@
map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
define_overloaded ("less_eq_" ^ tyname ^ "_def",
- mk_binrel_def @{const_name less_eq} p) ||>>
+ mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>
define_overloaded ("less_" ^ tyname ^ "_def",
- mk_binrel_def @{const_name less} p);
+ mk_binrel_def \<^const_name>\<open>less\<close> p);
val UNIV_eq = Goal.prove lthy [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -214,7 +214,7 @@
ALLGOALS (asm_full_simp_tac ctxt));
val finite_UNIV = Goal.prove lthy [] []
- (HOLogic.mk_Trueprop (Const (@{const_name finite},
+ (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,
HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
(fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
@@ -225,13 +225,13 @@
val range_pos = Goal.prove lthy [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Const (@{const_name image}, (T --> HOLogic.intT) -->
+ (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->
HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
p $ HOLogic.mk_UNIV T,
- Const (@{const_name atLeastLessThan}, HOLogic.intT -->
+ Const (\<^const_name>\<open>atLeastLessThan\<close>, HOLogic.intT -->
HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
HOLogic.mk_number HOLogic.intT 0 $
- (@{term int} $ card))))
+ (\<^term>\<open>int\<close> $ card))))
(fn {context = ctxt, ...} =>
simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
@@ -264,12 +264,12 @@
val first_el = Goal.prove lthy' [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Const (@{const_name first_el}, T), hd cs)))
+ (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))
(fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
val last_el = Goal.prove lthy' [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Const (@{const_name last_el}, T), List.last cs)))
+ (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))
(fn {context = ctxt, ...} =>
simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
in
@@ -414,43 +414,43 @@
| tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
- | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
+ | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
(fst (tm_of vs e), fst (tm_of vs e')), booleanN)
- | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
+ | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
(fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
- | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
+ | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
(fst (tm_of vs e), fst (tm_of vs e')), booleanN)
- | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
+ | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
(fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
- | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop @{const_name plus}
+ | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
- | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop @{const_name minus}
+ | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
- | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop @{const_name times}
+ | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
- | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop @{const_name divide}
+ | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
- | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
+ | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
- | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name modulo}
+ | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
| tm_of vs (Funct ("-", [e])) =
- (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)
+ (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
| tm_of vs (Funct ("**", [e, e'])) =
- (Const (@{const_name power}, HOLogic.intT --> HOLogic.natT -->
+ (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
HOLogic.intT) $ fst (tm_of vs e) $
- (@{const nat} $ fst (tm_of vs e')), integerN)
+ (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
| tm_of (tab, _) (Ident s) =
(case Symtab.lookup tab s of
@@ -528,7 +528,7 @@
(* enumeration type to integer *)
(case try (unsuffix "__pos") s of
SOME tyname => (case es of
- [e] => (Const (@{const_name pos},
+ [e] => (Const (\<^const_name>\<open>pos\<close>,
mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
integerN)
| _ => error ("Function " ^ s ^ " expects one argument"))
@@ -537,7 +537,7 @@
(* integer to enumeration type *)
(case try (unsuffix "__val") s of
SOME tyname => (case es of
- [e] => (Const (@{const_name val},
+ [e] => (Const (\<^const_name>\<open>val\<close>,
HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
tyname)
| _ => error ("Function " ^ s ^ " expects one argument"))
@@ -550,8 +550,8 @@
val (t, tyname) = tm_of vs e;
val T = mk_type thy prfx tyname
in (Const
- (if s = "succ" then @{const_name succ}
- else @{const_name pred}, T --> T) $ t, tyname)
+ (if s = "succ" then \<^const_name>\<open>succ\<close>
+ else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
end
| _ => error ("Function " ^ s ^ " expects one argument"))
@@ -580,7 +580,7 @@
val U = mk_type thy prfx elty;
val fT = T --> U
in
- (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $
+ (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
fst (tm_of vs e'),
ty)
@@ -628,7 +628,7 @@
val T = foldr1 HOLogic.mk_prodT Ts;
val U = mk_type thy prfx elty;
fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
- | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},
+ | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
T --> T --> HOLogic.mk_setT T) $
fst (tm_of vs e) $ fst (tm_of vs e');
fun mk_idx idx =
@@ -638,22 +638,22 @@
fun mk_upd (idxs, e) t =
if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
then
- Const (@{const_name fun_upd}, (T --> U) -->
+ Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
T --> U --> T --> U) $ t $
foldl1 HOLogic.mk_prod
(map (fst o tm_of vs o fst) (hd idxs)) $
fst (tm_of vs e)
else
- Const (@{const_name fun_upds}, (T --> U) -->
+ Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
HOLogic.mk_setT T --> U --> T --> U) $ t $
- foldl1 (HOLogic.mk_binop @{const_name sup})
+ foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
(map mk_idx idxs) $
fst (tm_of vs e)
in
(fold mk_upd assocs
(case default of
SOME e => Abs ("x", T, fst (tm_of vs e))
- | NONE => Const (@{const_name undefined}, T --> U)),
+ | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
s)
end
| _ => error (s ^ " is not an array type"))
@@ -973,7 +973,7 @@
\because their proofs contain oracles:" proved'));
val prv_path = Path.ext "prv" path;
val _ =
- if File.exists prv_path orelse Options.default_bool @{system_option spark_prv} then
+ if File.exists prv_path orelse Options.default_bool \<^system_option>\<open>spark_prv\<close> then
File.write prv_path
(implode (map (fn (s, _) => snd (strip_number s) ^
" -- proved by " ^ Distribution.version ^ "\n") proved''))
@@ -1096,8 +1096,8 @@
val (((defs', vars''), ivars), (ids, thy')) =
((Symtab.empty |>
- Symtab.update ("false", (@{term False}, booleanN)) |>
- Symtab.update ("true", (@{term True}, booleanN)),
+ Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
+ Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),
Name.context),
thy |> Sign.add_path
((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
--- a/src/Pure/ML/ml_console.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/ML/ml_console.scala Thu May 31 22:59:08 2018 +0200
@@ -54,8 +54,10 @@
if (!no_build && !raw_ml_system) {
val progress = new Console_Progress()
val rc =
- Build.build_logic(options, logic, build_heap = true, progress = progress,
- dirs = dirs, system_mode = system_mode)
+ progress.interrupt_handler {
+ Build.build_logic(options, logic, build_heap = true, progress = progress,
+ dirs = dirs, system_mode = system_mode)
+ }
if (rc != 0) sys.exit(rc)
}
--- a/src/Pure/PIDE/command.ML Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/command.ML Thu May 31 22:59:08 2018 +0200
@@ -22,6 +22,7 @@
val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
type print
+ val print0: (unit -> unit) -> eval -> print
val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
@@ -317,35 +318,39 @@
val overlay_ord = prod_ord string_ord (list_ord string_ord);
+fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval =
+ let
+ val exec_id = Document_ID.make ();
+ fun process () =
+ let
+ val {failed, command, state = st', ...} = eval_result eval;
+ val tr = Toplevel.exec_id exec_id command;
+ val opt_context = try Toplevel.generic_theory_of st';
+ in
+ if failed andalso strict then ()
+ else print_error tr opt_context (fn () => print_fn tr st')
+ end;
+ in
+ Print {
+ name = name, args = args, delay = delay, pri = pri, persistent = persistent,
+ exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
+ end;
+
+fun bad_print name_args exn =
+ make_print name_args {delay = NONE, pri = 0, persistent = false,
+ strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
+
in
+fun print0 e =
+ make_print ("", [serial_string ()])
+ {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
+
fun print command_visible command_overlays keywords command_name eval old_prints =
let
val print_functions = Synchronized.value print_functions;
- fun make_print name args {delay, pri, persistent, strict, print_fn} =
- let
- val exec_id = Document_ID.make ();
- fun process () =
- let
- val {failed, command, state = st', ...} = eval_result eval;
- val tr = Toplevel.exec_id exec_id command;
- val opt_context = try Toplevel.generic_theory_of st';
- in
- if failed andalso strict then ()
- else print_error tr opt_context (fn () => print_fn tr st')
- end;
- in
- Print {
- name = name, args = args, delay = delay, pri = pri, persistent = persistent,
- exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
- end;
-
- fun bad_print name args exn =
- make_print name args {delay = NONE, pri = 0, persistent = false,
- strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
-
- fun new_print name args get_pr =
+ fun new_print (name, args) get_pr =
let
val params =
{keywords = keywords,
@@ -355,31 +360,36 @@
in
(case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
Exn.Res NONE => NONE
- | Exn.Res (SOME pr) => SOME (make_print name args pr)
- | Exn.Exn exn => SOME (bad_print name args exn))
+ | Exn.Res (SOME pr) => SOME (make_print (name, args) pr eval)
+ | Exn.Exn exn => SOME (bad_print (name, args) exn eval))
end;
- fun get_print (a, b) =
- (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
+ fun get_print (name, args) =
+ (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of
NONE =>
- (case AList.lookup (op =) print_functions a of
- NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a)))
- | SOME get_pr => new_print a b get_pr)
+ (case AList.lookup (op =) print_functions name of
+ NONE =>
+ SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval)
+ | SOME get_pr => new_print (name, args) get_pr)
| some => some);
- val new_prints =
+ val retained_prints =
+ filter (fn print => print_finished print andalso print_persistent print) old_prints;
+ val visible_prints =
if command_visible then
- fold (fn (a, _) => cons (a, [])) print_functions command_overlays
+ fold (fn (name, _) => cons (name, [])) print_functions command_overlays
|> sort_distinct overlay_ord
|> map_filter get_print
- else filter (fn print => print_finished print andalso print_persistent print) old_prints;
+ else [];
+ val new_prints = visible_prints @ retained_prints;
in
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
end;
fun print_function name f =
Synchronized.change print_functions (fn funs =>
- (if not (AList.defined (op =) funs name) then ()
+ (if name = "" then error "Unnamed print function" else ();
+ if not (AList.defined (op =) funs name) then ()
else warning ("Redefining command print function: " ^ quote name);
AList.update (op =) (name, f) funs));
--- a/src/Pure/PIDE/command.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/command.scala Thu May 31 22:59:08 2018 +0200
@@ -261,9 +261,7 @@
markups: Markups = Markups.empty)
{
def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
-
- lazy val consolidated: Boolean =
- status.exists(markup => markup.name == Markup.CONSOLIDATED)
+ def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
lazy val protocol_status: Protocol.Status =
{
--- a/src/Pure/PIDE/document.ML Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/document.ML Thu May 31 22:59:08 2018 +0200
@@ -24,8 +24,7 @@
val command_exec: state -> string -> Document_ID.command -> Command.exec option
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
- val consolidate_execution: state -> unit
- val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
+ val update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state ->
Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
val state: unit -> state
val change_state: (state -> state) -> unit
@@ -55,24 +54,22 @@
structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
-type consolidation = (int -> int option) * Thy_Output.segment list;
-
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
keywords: Keyword.keywords option, (*outer syntax keywords*)
perspective: perspective, (*command perspective*)
entries: Command.exec option Entries.T, (*command entries with executions*)
- result: Command.eval option, (*result of last execution*)
- consolidation: consolidation future} (*consolidation status of eval forks*)
+ result: (Document_ID.command * Command.eval) option, (*result of last execution*)
+ consolidated: unit lazy} (*consolidated status of eval forks*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
-fun make_node (header, keywords, perspective, entries, result, consolidation) =
+fun make_node (header, keywords, perspective, entries, result, consolidated) =
Node {header = header, keywords = keywords, perspective = perspective,
- entries = entries, result = result, consolidation = consolidation};
+ entries = entries, result = result, consolidated = consolidated};
-fun map_node f (Node {header, keywords, perspective, entries, result, consolidation}) =
- make_node (f (header, keywords, perspective, entries, result, consolidation));
+fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
+ make_node (f (header, keywords, perspective, entries, result, consolidated));
fun make_perspective (required, command_ids, overlays) : perspective =
{required = required,
@@ -85,7 +82,7 @@
val no_perspective = make_perspective (false, [], []);
val empty_node =
- make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Future.value (K NONE, []));
+ make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
not required andalso
@@ -93,13 +90,13 @@
is_none visible_last andalso
Inttab.is_empty overlays;
-fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidation}) =
+fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
header = no_header andalso
is_none keywords andalso
is_no_perspective perspective andalso
Entries.is_empty entries andalso
is_none result andalso
- Future.is_finished consolidation;
+ Lazy.is_finished consolidated;
(* basic components *)
@@ -110,15 +107,15 @@
| _ => Path.current);
fun set_header master header errors =
- map_node (fn (_, keywords, perspective, entries, result, consolidation) =>
+ map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
({master = master, header = header, errors = errors},
- keywords, perspective, entries, result, consolidation));
+ keywords, perspective, entries, result, consolidated));
fun get_header (Node {header, ...}) = header;
fun set_keywords keywords =
- map_node (fn (header, _, perspective, entries, result, consolidation) =>
- (header, keywords, perspective, entries, result, consolidation));
+ map_node (fn (header, _, perspective, entries, result, consolidated) =>
+ (header, keywords, perspective, entries, result, consolidated));
fun get_keywords (Node {keywords, ...}) = keywords;
@@ -142,8 +139,8 @@
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective args =
- map_node (fn (header, keywords, _, entries, result, consolidation) =>
- (header, keywords, make_perspective args, entries, result, consolidation));
+ map_node (fn (header, keywords, _, entries, result, consolidated) =>
+ (header, keywords, make_perspective args, entries, result, consolidated));
val required_node = #required o get_perspective;
val visible_command = Inttab.defined o #visible o get_perspective;
@@ -152,8 +149,8 @@
val overlays = Inttab.lookup_list o #overlays o get_perspective;
fun map_entries f =
- map_node (fn (header, keywords, perspective, entries, result, consolidation) =>
- (header, keywords, perspective, f entries, result, consolidation));
+ map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
+ (header, keywords, perspective, f entries, result, consolidated));
fun get_entries (Node {entries, ...}) = entries;
@@ -166,30 +163,40 @@
fun get_result (Node {result, ...}) = result;
fun set_result result =
- map_node (fn (header, keywords, perspective, entries, _, consolidation) =>
- (header, keywords, perspective, entries, result, consolidation));
+ map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
+ (header, keywords, perspective, entries, result, consolidated));
fun pending_result node =
(case get_result node of
- SOME eval => not (Command.eval_finished eval)
+ SOME (_, eval) => not (Command.eval_finished eval)
| NONE => false);
fun finished_result node =
(case get_result node of
- SOME eval => Command.eval_finished eval
+ SOME (_, eval) => Command.eval_finished eval
| NONE => false);
fun finished_result_theory node =
if finished_result node then
- let val st = Command.eval_result_state (the (get_result node))
- in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
+ let
+ val (result_id, eval) = the (get_result node);
+ val st = Command.eval_result_state eval;
+ in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
else NONE;
-val reset_consolidation =
+val reset_consolidated =
map_node (fn (header, keywords, perspective, entries, result, _) =>
- (header, keywords, perspective, entries, result, Future.promise I));
+ (header, keywords, perspective, entries, result, Lazy.lazy I));
+
+fun get_consolidated (Node {consolidated, ...}) = consolidated;
+
+val is_consolidated = Lazy.is_finished o get_consolidated;
-fun get_consolidation (Node {consolidation, ...}) = consolidation;
+fun commit_consolidated node =
+ (Lazy.force (get_consolidated node); Output.status (Markup.markup_only Markup.consolidated));
+
+fun could_consolidate node =
+ not (is_consolidated node) andalso is_some (finished_result_theory node);
fun get_node nodes name = String_Graph.get_node nodes name
handle String_Graph.UNDEF _ => empty_node;
@@ -414,9 +421,6 @@
val the_command_name = #1 oo the_command;
-fun force_command_span state =
- Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
-
(* execution *)
@@ -515,77 +519,6 @@
{version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
in (versions, blobs, commands, execution') end));
-fun presentation options thy node_name node =
- if Options.bool options "editor_presentation" then
- let
- val (adjust, segments) = Future.get_finished (get_consolidation node);
- val presentation_context: Thy_Info.presentation_context =
- {options = options,
- file_pos = Position.file node_name,
- adjust_pos = Position.adjust_offsets adjust,
- segments = segments};
- in Thy_Info.apply_presentation presentation_context thy end
- else ();
-
-fun consolidate_execution state =
- let
- fun check_consolidation node_name node =
- if Future.is_finished (get_consolidation node) then ()
- else
- (case finished_result_theory node of
- NONE => ()
- | SOME thy =>
- let
- val result_id = Command.eval_exec_id (the (get_result node));
- val eval_ids =
- iterate_entries (fn (_, opt_exec) => fn eval_ids =>
- (case opt_exec of
- SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
- | NONE => NONE)) node [];
- in
- (case Execution.snapshot eval_ids of
- [] =>
- let
- val (_, offsets, rev_segments) =
- iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
- (case opt_exec of
- SOME (eval, _) =>
- let
- val command_id = Command.eval_command_id eval;
- val span = force_command_span state command_id;
-
- val exec_id = Command.eval_exec_id eval;
- val tr = Command.eval_result_command eval;
- val st' = Command.eval_result_state eval;
-
- val offset' = offset + the_default 0 (Command_Span.symbol_length span);
- val offsets' = offsets
- |> Inttab.update (command_id, offset)
- |> Inttab.update (exec_id, offset);
- val segments' = (span, tr, st') :: segments;
- in SOME (offset', offsets', segments') end
- | NONE => NONE)) node (0, Inttab.empty, []);
-
- val adjust = Inttab.lookup offsets;
- val segments =
- rev rev_segments |> map (fn (span, tr, st') =>
- {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
-
- val _ = Future.fulfill (get_consolidation node) (adjust, segments);
- val _ =
- Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
- (fn () =>
- (Output.status (Markup.markup_only Markup.consolidated);
- (* FIXME avoid user operations on protocol thread *)
- presentation (Options.default ()) thy node_name node)) ();
- in () end
- | _ => ())
- end);
- in
- String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidation node_name node)
- (nodes_of (get_execution_version state)) ()
- end;
-
(** document update **)
@@ -596,6 +529,7 @@
val assign_update_empty: assign_update = Inttab.empty;
fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
+fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab;
fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
fun assign_update_new upd (tab: assign_update) =
@@ -626,7 +560,7 @@
maybe_end_theory pos
(case get_result (snd (the (AList.lookup (op =) deps import))) of
NONE => Toplevel.toplevel
- | SOME eval => Command.eval_result_state eval)
+ | SOME (_, eval) => Command.eval_result_state eval)
| some => some)
|> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
@@ -727,10 +661,78 @@
fun removed_execs node0 (command_id, exec_ids) =
subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
+fun print_consolidation options the_command_span node_name (assign_update, node) =
+ (case finished_result_theory node of
+ SOME (result_id, thy) =>
+ let
+ val eval_ids =
+ iterate_entries (fn (_, opt_exec) => fn eval_ids =>
+ (case opt_exec of
+ SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
+ | NONE => NONE)) node [];
+ in
+ if null (Execution.snapshot eval_ids) then
+ let
+ val consolidation =
+ if Options.bool options "editor_presentation" then
+ let
+ val (_, offsets, rev_segments) =
+ iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
+ (case opt_exec of
+ SOME (eval, _) =>
+ let
+ val command_id = Command.eval_command_id eval;
+ val span = the_command_span command_id;
+
+ val exec_id = Command.eval_exec_id eval;
+ val tr = Command.eval_result_command eval;
+ val st' = Command.eval_result_state eval;
+
+ val offset' = offset + the_default 0 (Command_Span.symbol_length span);
+ val offsets' = offsets
+ |> Inttab.update (command_id, offset)
+ |> Inttab.update (exec_id, offset);
+ val segments' = (span, tr, st') :: segments;
+ in SOME (offset', offsets', segments') end
+ | NONE => NONE)) node (0, Inttab.empty, []);
+
+ val adjust = Inttab.lookup offsets;
+ val segments =
+ rev rev_segments |> map (fn (span, tr, st') =>
+ {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
+
+ val presentation_context: Thy_Info.presentation_context =
+ {options = options,
+ file_pos = Position.file node_name,
+ adjust_pos = Position.adjust_offsets adjust,
+ segments = segments};
+ in
+ fn () =>
+ (Thy_Info.apply_presentation presentation_context thy;
+ commit_consolidated node)
+ end
+ else fn () => commit_consolidated node;
+
+ val result_entry =
+ (case lookup_entry node result_id of
+ NONE => err_undef "result command entry" result_id
+ | SOME (eval, prints) =>
+ (result_id, SOME (eval, Command.print0 consolidation eval :: prints)));
+
+ val assign_update' = assign_update |> assign_update_change result_entry;
+ val node' = node |> assign_entry result_entry;
+ in (assign_update', node') end
+ else (assign_update, node)
+ end
+ | NONE => (assign_update, node));
in
-fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () =>
+fun update old_version_id new_version_id edits consolidate state =
+ Runtime.exn_trace_system (fn () =>
let
+ val options = Options.default ();
+ val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
+
val old_version = the_version state old_version_id;
val new_version =
timeit "Document.edit_nodes"
@@ -753,12 +755,15 @@
let
val root_theory = check_root_theory node;
val keywords = the_default (Session.get_keywords ()) (get_keywords node);
+
+ val maybe_consolidate = consolidate andalso could_consolidate node;
val imports = map (apsnd Future.join) deps;
val imports_result_changed = exists (#4 o #1 o #2) imports;
val node_required = Symtab.defined required name;
in
- if Symtab.defined edited name orelse visible_node node orelse
- imports_result_changed orelse Symtab.defined required0 name <> node_required
+ if Symtab.defined edited name orelse maybe_consolidate orelse
+ visible_node node orelse imports_result_changed orelse
+ Symtab.defined required0 name <> node_required
then
let
val node0 = node_of old_version name;
@@ -785,7 +790,7 @@
if not node_required andalso prev = visible_last node then NONE
else new_exec keywords state node proper_init id res) node;
- val assigned_execs =
+ val assign_update =
(node0, updated_execs) |-> iterate_entries_after common
(fn ((_, command_id0), exec0) => fn res =>
if is_none exec0 then NONE
@@ -796,32 +801,36 @@
if command_id' = Document_ID.none then NONE else SOME command_id';
val result =
if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
- else SOME (#1 exec');
-
- val assign_update = assign_update_result assigned_execs;
- val removed = maps (removed_execs node0) assign_update;
- val _ = List.app Execution.cancel removed;
+ else SOME (command_id', #1 exec');
val result_changed =
- not (eq_option Command.eval_eq (get_result node0, result));
- val node' = node
- |> assign_update_apply assigned_execs
+ not (eq_option (Command.eval_eq o apply2 #2) (get_result node0, result));
+ val (assign_update', node') = node
+ |> assign_update_apply assign_update
|> set_result result
- |> result_changed ? reset_consolidation;
+ |> result_changed ? reset_consolidated
+ |> pair assign_update
+ |> (not result_changed andalso maybe_consolidate) ?
+ print_consolidation options the_command_span name;
+
+ val assign_result = assign_update_result assign_update';
+ val removed = maps (removed_execs node0) assign_result;
+ val _ = List.app Execution.cancel removed;
+
val assigned_node = SOME (name, node');
- in ((removed, assign_update, assigned_node, result_changed), node') end
+ in ((removed, assign_result, assigned_node, result_changed), node') end
else (([], [], NONE, false), node)
end))))
|> Future.joins |> map #1);
val removed = maps #1 updated;
- val assign_update = maps #2 updated;
+ val assign_result = maps #2 updated;
val assigned_nodes = map_filter #3 updated;
val state' = state
|> define_version new_version_id (fold put_node assigned_nodes new_version);
- in (removed, assign_update, state') end);
+ in (removed, assign_result, state') end);
end;
--- a/src/Pure/PIDE/document.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/document.scala Thu May 31 22:59:08 2018 +0200
@@ -930,8 +930,10 @@
def node_consolidated(version: Version, name: Node.Name): Boolean =
!name.is_theory ||
- version.nodes(name).commands.reverse.iterator.
- flatMap(command_states(version, _)).exists(_.consolidated)
+ {
+ val it = version.nodes(name).commands.reverse.iterator
+ it.hasNext && command_states(version, it.next).exists(_.consolidated)
+ }
// persistent user-view
def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
--- a/src/Pure/PIDE/protocol.ML Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu May 31 22:59:08 2018 +0200
@@ -64,10 +64,6 @@
end);
val _ =
- Isabelle_Process.protocol_command "Document.consolidate_execution"
- (fn [] => Document.consolidate_execution (Document.state ()));
-
-val _ =
Isabelle_Process.protocol_command "Document.discontinue_execution"
(fn [] => Execution.discontinue ());
@@ -78,49 +74,52 @@
val _ =
Isabelle_Process.protocol_command "Document.update"
(Future.task_context "Document.update" (Future.new_group NONE)
- (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
- let
- val _ = Execution.discontinue ();
+ (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] =>
+ Document.change_state (fn state =>
+ let
+ val old_id = Document_ID.parse old_id_string;
+ val new_id = Document_ID.parse new_id_string;
+ val edits =
+ YXML.parse_body edits_yxml |>
+ let open XML.Decode in
+ list (pair string
+ (variant
+ [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+ fn ([], a) =>
+ let
+ val (master, (name, (imports, (keywords, errors)))) =
+ pair string (pair string (pair (list string)
+ (pair (list (pair string
+ (pair (pair string (list string)) (list string))))
+ (list YXML.string_of_body)))) a;
+ val imports' = map (rpair Position.none) imports;
+ val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+ val header = Thy_Header.make (name, Position.none) imports' keywords';
+ in Document.Deps {master = master, header = header, errors = errors} end,
+ fn (a :: b, c) =>
+ Document.Perspective (bool_atom a, map int_atom b,
+ list (pair int (pair string (list string))) c)]))
+ end;
+ val consolidate = Value.parse_bool consolidate_string;
- val old_id = Document_ID.parse old_id_string;
- val new_id = Document_ID.parse new_id_string;
- val edits =
- YXML.parse_body edits_yxml |>
- let open XML.Decode in
- list (pair string
- (variant
- [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
- fn ([], a) =>
- let
- val (master, (name, (imports, (keywords, errors)))) =
- pair string (pair string (pair (list string)
- (pair (list (pair string
- (pair (pair string (list string)) (list string))))
- (list YXML.string_of_body)))) a;
- val imports' = map (rpair Position.none) imports;
- val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
- val header = Thy_Header.make (name, Position.none) imports' keywords';
- in Document.Deps {master = master, header = header, errors = errors} end,
- fn (a :: b, c) =>
- Document.Perspective (bool_atom a, map int_atom b,
- list (pair int (pair string (list string))) c)]))
- end;
+ val _ = Execution.discontinue ();
- val (removed, assign_update, state') = Document.update old_id new_id edits state;
- val _ =
- (singleton o Future.forks)
- {name = "Document.update/remove", group = NONE,
- deps = Execution.snapshot removed,
- pri = Task_Queue.urgent_pri + 2, interrupts = false}
- (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
+ val (removed, assign_update, state') =
+ Document.update old_id new_id edits consolidate state;
+ val _ =
+ (singleton o Future.forks)
+ {name = "Document.update/remove", group = NONE,
+ deps = Execution.snapshot removed,
+ pri = Task_Queue.urgent_pri + 2, interrupts = false}
+ (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
- val _ =
- Output.protocol_message Markup.assign_update
- [(new_id, assign_update) |>
- let open XML.Encode
- in pair int (list (pair int (list int))) end
- |> YXML.string_of_body];
- in Document.start_execution state' end)));
+ val _ =
+ Output.protocol_message Markup.assign_update
+ [(new_id, assign_update) |>
+ let open XML.Encode
+ in pair int (list (pair int (list int))) end
+ |> YXML.string_of_body];
+ in Document.start_execution state' end)));
val _ =
Isabelle_Process.protocol_command "Document.remove_versions"
--- a/src/Pure/PIDE/protocol.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu May 31 22:59:08 2018 +0200
@@ -409,9 +409,6 @@
/* execution */
- def consolidate_execution(): Unit =
- protocol_command("Document.consolidate_execution")
-
def discontinue_execution(): Unit =
protocol_command("Document.discontinue_execution")
@@ -422,7 +419,7 @@
/* document versions */
def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
- edits: List[Document.Edit_Command])
+ edits: List[Document.Edit_Command], consolidate: Boolean)
{
val edits_yxml =
{
@@ -450,7 +447,8 @@
pair(string, encode_edit(name))(name.node, edit)
})
Symbol.encode_yxml(encode_edits(edits)) }
- protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
+ protocol_command(
+ "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString)
}
def remove_versions(versions: List[Document.Version])
--- a/src/Pure/PIDE/resources.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/resources.scala Thu May 31 22:59:08 2018 +0200
@@ -215,8 +215,9 @@
reparse_limit: Int,
previous: Document.Version,
doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): Session.Change =
- Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits)
+ edits: List[Document.Edit_Text],
+ consolidate: Boolean): Session.Change =
+ Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
def commit(change: Session.Change) { }
--- a/src/Pure/PIDE/session.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/PIDE/session.scala Thu May 31 22:59:08 2018 +0200
@@ -50,6 +50,7 @@
syntax_changed: List[Document.Node.Name],
deps_changed: Boolean,
doc_edits: List[Document.Edit_Command],
+ consolidate: Boolean,
version: Document.Version)
case object Change_Flush
@@ -230,15 +231,16 @@
previous: Future[Document.Version],
doc_blobs: Document.Blobs,
text_edits: List[Document.Edit_Text],
+ consolidate: Boolean,
version_result: Promise[Document.Version])
private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
{
- case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
+ case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
val prev = previous.get_finished
val change =
Timing.timeit("parse_change", timing) {
- resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
+ resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
}
version_result.fulfill(change.version)
manager.send(change)
@@ -342,7 +344,10 @@
{
/* raw edits */
- def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+ def handle_raw_edits(
+ doc_blobs: Document.Blobs = Document.Blobs.empty,
+ edits: List[Document.Edit_Text] = Nil,
+ consolidate: Boolean = false)
//{{{
{
require(prover.defined)
@@ -354,7 +359,7 @@
global_state.change(_.continue_history(previous, edits, version))
raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
- change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
+ change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
}
//}}}
@@ -392,7 +397,7 @@
val assignment = global_state.value.the_assignment(change.previous).check_finished
global_state.change(_.define_version(change.version, assignment))
- prover.get.update(change.previous.id, change.version.id, change.doc_edits)
+ prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
resources.commit(change)
}
//}}}
@@ -529,7 +534,7 @@
}
case Consolidate_Execution =>
- if (prover.defined) prover.get.consolidate_execution()
+ if (prover.defined) handle_raw_edits(consolidate = true)
case Prune_History =>
if (prover.defined) {
@@ -540,7 +545,7 @@
case Update_Options(options) =>
if (prover.defined && is_ready) {
prover.get.options(options)
- handle_raw_edits(Document.Blobs.empty, Nil)
+ handle_raw_edits()
}
global_options.post(Session.Global_Options(options))
@@ -548,7 +553,7 @@
prover.get.cancel_exec(exec_id)
case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
- handle_raw_edits(doc_blobs, edits)
+ handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
case Session.Dialog_Result(id, serial, result) if prover.defined =>
prover.get.dialog_result(serial, result)
--- a/src/Pure/System/progress.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/System/progress.scala Thu May 31 22:59:08 2018 +0200
@@ -51,7 +51,10 @@
}
override def theory(session: String, theory: String): Unit =
- if (verbose) echo(session + ": theory " + theory)
+ if (verbose) {
+ if (session == "") echo("theory " + theory)
+ else echo(session + ": theory " + theory)
+ }
@volatile private var is_stopped = false
override def interrupt_handler[A](e: => A): A =
--- a/src/Pure/Thy/export.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Thy/export.scala Thu May 31 22:59:08 2018 +0200
@@ -288,8 +288,10 @@
if (!no_build) {
val rc =
- Build.build_logic(options, session_name, progress = progress,
- dirs = dirs, system_mode = system_mode)
+ progress.interrupt_handler {
+ Build.build_logic(options, session_name, progress = progress,
+ dirs = dirs, system_mode = system_mode)
+ }
if (rc != 0) sys.exit(rc)
}
--- a/src/Pure/Thy/thy_resources.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Thu May 31 22:59:08 2018 +0200
@@ -144,9 +144,32 @@
Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
{ if (progress.stopped) result.cancel else check_state }
+ val theories_progress = Synchronized(Set.empty[Document.Node.Name])
+
val consumer =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
- case changed => if (dep_theories.exists(changed.nodes)) check_state
+ case changed =>
+ if (dep_theories.exists(changed.nodes)) {
+
+ val check_theories =
+ (for (command <- changed.commands.iterator if command.potentially_initialized)
+ yield command.node_name).toSet
+
+ if (check_theories.nonEmpty) {
+ val snapshot = session.snapshot()
+ val initialized =
+ theories_progress.change_result(theories =>
+ {
+ val initialized =
+ (check_theories -- theories).toList.filter(name =>
+ Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
+ (initialized, theories ++ initialized)
+ })
+ initialized.map(_.theory).sorted.foreach(progress.theory("", _))
+ }
+
+ check_state
+ }
}
try {
--- a/src/Pure/Thy/thy_syntax.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Thu May 31 22:59:08 2018 +0200
@@ -296,7 +296,8 @@
reparse_limit: Int,
previous: Document.Version,
doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): Session.Change =
+ edits: List[Document.Edit_Text],
+ consolidate: Boolean): Session.Change =
{
val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
@@ -356,6 +357,7 @@
(doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
}
- Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version)
+ Session.Change(
+ previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version)
}
}
--- a/src/Pure/Tools/build.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Tools/build.scala Thu May 31 22:59:08 2018 +0200
@@ -836,10 +836,8 @@
system_mode = system_mode, sessions = List(logic)).ok) 0
else {
progress.echo("Build started for Isabelle/" + logic + " ...")
- progress.interrupt_handler {
- Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
- system_mode = system_mode, sessions = List(logic)).rc
- }
+ Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
+ system_mode = system_mode, sessions = List(logic)).rc
}
}
}
--- a/src/Pure/Tools/dump.scala Thu May 31 10:59:54 2018 +0200
+++ b/src/Pure/Tools/dump.scala Thu May 31 22:59:08 2018 +0200
@@ -21,32 +21,28 @@
Bytes.write(path, bytes)
}
- def write(node_name: Document.Node.Name, file_name: String, text: String)
- {
+ def write(node_name: Document.Node.Name, file_name: String, text: String): Unit =
write(node_name, file_name, Bytes(text))
- }
+
+ def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit =
+ write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
}
sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
private val known_aspects =
List(
- Aspect("list", "list theory nodes",
- { case args =>
- for (node_name <- args.result.node_names) args.progress.echo(node_name.toString)
- }),
Aspect("messages", "output messages (YXML format)",
{ case args =>
for (node_name <- args.result.node_names) {
args.write(node_name, "messages.yxml",
- YXML.string_of_body(args.result.messages(node_name).iterator.map(_._1).toList))
+ args.result.messages(node_name).iterator.map(_._1).toList)
}
}),
Aspect("markup", "PIDE markup (YXML format)",
{ case args =>
for (node_name <- args.result.node_names) {
- args.write(node_name, "markup.yxml",
- YXML.string_of_body(args.result.markup_to_XML(node_name)))
+ args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name))
}
})
)
@@ -176,21 +172,23 @@
val progress = new Console_Progress(verbose = verbose)
val result =
- dump(options, logic,
- aspects = aspects,
- progress = progress,
- dirs = dirs,
- select_dirs = select_dirs,
- output_dir = output_dir,
- verbose = verbose,
- selection = Sessions.Selection(
- requirements = requirements,
- all_sessions = all_sessions,
- base_sessions = base_sessions,
- exclude_session_groups = exclude_session_groups,
- exclude_sessions = exclude_sessions,
- session_groups = session_groups,
- sessions = sessions))
+ progress.interrupt_handler {
+ dump(options, logic,
+ aspects = aspects,
+ progress = progress,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ output_dir = output_dir,
+ verbose = verbose,
+ selection = Sessions.Selection(
+ requirements = requirements,
+ all_sessions = all_sessions,
+ base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups,
+ exclude_sessions = exclude_sessions,
+ session_groups = session_groups,
+ sessions = sessions))
+ }
progress.echo(result.timing.message_resources)