--- a/NEWS Sat Jun 02 22:57:18 2018 +0100
+++ b/NEWS Sat Jun 02 22:57:44 2018 +0100
@@ -380,6 +380,11 @@
and concurrent use of theories, based on Isabelle/PIDE infrastructure.
See also the "system" manual.
+* The command-line tool "dump" dumps information from the cumulative
+PIDE session database: many sessions may be loaded into a given logic
+image, results from all loaded theories are written to the output
+directory.
+
* The command-line tool "isabelle update_comments" normalizes formal
comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
approximate the appearance in document output). This is more specific
--- a/etc/options Sat Jun 02 22:57:18 2018 +0100
+++ b/etc/options Sat Jun 02 22:57:44 2018 +0100
@@ -156,7 +156,7 @@
public option editor_output_delay : real = 0.1
-- "delay for prover output (markup, common messages etc.)"
-public option editor_consolidate_delay : real = 1.0
+public option editor_consolidate_delay : real = 2.5
-- "delay to consolidate status of command evaluation (execution forks)"
public option editor_prune_delay : real = 15
--- a/src/Doc/System/Sessions.thy Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Doc/System/Sessions.thy Sat Jun 02 22:57:44 2018 +0100
@@ -595,4 +595,85 @@
own sub-directory hierarchy, using the session-qualified theory name.
\<close>
+
+section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
+
+text \<open>
+ The @{tool_def "dump"} tool dumps information from the cumulative PIDE
+ session database (which is processed on the spot). Its command-line usage
+ is: @{verbatim [display]
+\<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -A NAMES dump named aspects (default: ...)
+ -B NAME include session NAME and all descendants
+ -D DIR include session directory and select its sessions
+ -O DIR output directory for dumped files (default: "dump")
+ -R operate on requirements of selected sessions
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -l NAME logic session name (default ISABELLE_LOGIC="HOL")
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -s system build mode for logic image
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Dump cumulative PIDE session database, with the following aspects:
+ ...\<close>}
+
+ \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
+ remaining command-line arguments specify sessions as in @{tool build}
+ (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
+ theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
+ in the current directory).
+
+ \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
+ its theories are not processed again, and their PIDE session database is
+ excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
+ the logic image (\secref{sec:tool-build}).
+
+ \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
+ (\secref{sec:tool-build}).
+
+ \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
+
+ \<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
+ list. The default is to dump all known aspects, as given in the command-line
+ usage of the tool. The underlying Isabelle/Scala function
+ \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
+ final PIDE state and document version. This allows to imitate Prover IDE
+ rendering under program control.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Dump all Isabelle/ZF sessions (which are rather small):
+ @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
+
+ \<^smallskip>
+ Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
+ as starting point:
+ @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
+
+ \<^smallskip>
+ Dump all sessions connected to HOL-Analysis, including a full bootstrap of
+ Isabelle/HOL from Isabelle/Pure:
+ @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
+
+ This results in uniform PIDE markup for everything, except for the
+ Isabelle/Pure bootstrap process itself. Producing that on the spot requires
+ several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
+ process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
+ for such ambitious applications:
+ @{verbatim [display]
+\<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
+ML_OPTIONS="--minheap 4G --maxheap 32G"
+\<close>}
+
+\<close>
+
end
--- a/src/HOL/Data_Structures/AVL_Set.thy Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy Sat Jun 02 22:57:44 2018 +0100
@@ -455,7 +455,7 @@
subsection \<open>Height-Size Relation\<close>
-text \<open>By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
+text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
lemma height_invers:
"(height t = 0) = (t = Leaf)"
@@ -529,19 +529,36 @@
text \<open>The size of an AVL tree is (at least) exponential in its height:\<close>
-lemma avl_lowerbound:
+lemma avl_size_lowerbound:
defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
assumes "avl t"
- shows "real (size1 t) \<ge> \<phi> ^ (height t)"
+ shows "\<phi> ^ (height t) \<le> size1 t"
proof -
have "\<phi> > 0" by(simp add: \<phi>_def add_pos_nonneg)
hence "\<phi> ^ height t = (1 / \<phi> ^ 2) * \<phi> ^ (height t + 2)"
by(simp add: field_simps power2_eq_square)
- also have "\<dots> \<le> real (fib (height t + 2))"
+ also have "\<dots> \<le> fib (height t + 2)"
using fib_lowerbound[of "height t + 2"] by(simp add: \<phi>_def)
- also have "\<dots> \<le> real (size1 t)"
+ also have "\<dots> \<le> size1 t"
using avl_fib_bound[of t "height t"] assms by simp
finally show ?thesis .
qed
+text \<open>The height of an AVL tree is most @{term "(1/log 2 \<phi>)"} \<open>\<approx> 1.44\<close> times worse
+than @{term "log 2 (size1 t)"}:\<close>
+
+lemma avl_height_upperbound:
+ defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+ assumes "avl t"
+ shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)"
+proof -
+ have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
+ hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
+ also have "\<dots> \<le> log \<phi> (size1 t)"
+ using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> by simp
+ also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
+ by(simp add: log_base_change[of 2 \<phi>])
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/HOLCF/Domain.thy Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/HOLCF/Domain.thy Sat Jun 02 22:57:44 2018 +0100
@@ -341,12 +341,12 @@
setup \<open>
fold Domain_Take_Proofs.add_rec_type
- [(@{type_name cfun}, [true, true]),
- (@{type_name "sfun"}, [true, true]),
- (@{type_name ssum}, [true, true]),
- (@{type_name sprod}, [true, true]),
- (@{type_name prod}, [true, true]),
- (@{type_name "u"}, [true])]
+ [(\<^type_name>\<open>cfun\<close>, [true, true]),
+ (\<^type_name>\<open>sfun\<close>, [true, true]),
+ (\<^type_name>\<open>ssum\<close>, [true, true]),
+ (\<^type_name>\<open>sprod\<close>, [true, true]),
+ (\<^type_name>\<open>prod\<close>, [true, true]),
+ (\<^type_name>\<open>u\<close>, [true])]
\<close>
end
--- a/src/HOL/HOLCF/Map_Functions.thy Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy Sat Jun 02 22:57:44 2018 +0100
@@ -188,14 +188,14 @@
lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
apply standard
- subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse)
- subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below)
+ subgoal for x by (cases x) (simp_all add: ep_pair.e_inverse)
+ subgoal for y by (cases y) (simp_all add: ep_pair.e_p_below)
done
lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
apply standard
- subgoal for x by (cases x, simp, simp add: deflation.idem)
- subgoal for x by (cases x, simp, simp add: deflation.below)
+ subgoal for x by (cases x) (simp_all add: deflation.idem)
+ subgoal for x by (cases x) (simp_all add: deflation.below)
done
lemma finite_deflation_u_map:
@@ -235,12 +235,17 @@
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
- apply (induct p)
- apply simp
- apply (case_tac "f2\<cdot>x = \<bottom>", simp)
- apply (case_tac "g2\<cdot>y = \<bottom>", simp)
- apply simp
- done
+proof (induct p)
+ case bottom
+ then show ?case by simp
+next
+ case (spair x y)
+ then show ?case
+ apply (cases "f2\<cdot>x = \<bottom>", simp)
+ apply (cases "g2\<cdot>y = \<bottom>", simp)
+ apply simp
+ done
+qed
lemma ep_pair_sprod_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -251,11 +256,17 @@
show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
by (induct x) simp_all
show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
- apply (induct y)
- apply simp
- apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
- apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
- done
+ proof (induct y)
+ case bottom
+ then show ?case by simp
+ next
+ case (spair x y)
+ then show ?case
+ apply simp
+ apply (cases "p1\<cdot>x = \<bottom>", simp, cases "p2\<cdot>y = \<bottom>", simp)
+ apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
+ done
+ qed
qed
lemma deflation_sprod_map:
@@ -266,14 +277,24 @@
interpret d2: deflation d2 by fact
fix x
show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
- apply (induct x, simp)
- apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
- apply (simp add: d1.idem d2.idem)
- done
+ proof (induct x)
+ case bottom
+ then show ?case by simp
+ next
+ case (spair x y)
+ then show ?case
+ apply (cases "d1\<cdot>x = \<bottom>", simp, cases "d2\<cdot>y = \<bottom>", simp)
+ apply (simp add: d1.idem d2.idem)
+ done
+ qed
show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
- apply (induct x, simp)
- apply (simp add: monofun_cfun d1.below d2.below)
- done
+ proof (induct x)
+ case bottom
+ then show ?case by simp
+ next
+ case spair
+ then show ?case by (simp add: monofun_cfun d1.below d2.below)
+ qed
qed
lemma finite_deflation_sprod_map:
@@ -319,11 +340,16 @@
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
- apply (induct p)
- apply simp
- apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
- apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
- done
+proof (induct p)
+ case bottom
+ then show ?case by simp
+next
+ case (sinl x)
+ then show ?case by (cases "f2\<cdot>x = \<bottom>") simp_all
+next
+ case (sinr y)
+ then show ?case by (cases "g2\<cdot>y = \<bottom>") simp_all
+qed
lemma ep_pair_ssum_map:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -334,11 +360,16 @@
show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
by (induct x) simp_all
show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
- apply (induct y)
- apply simp
- apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
- apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
- done
+ proof (induct y)
+ case bottom
+ then show ?case by simp
+ next
+ case (sinl x)
+ then show ?case by (cases "p1\<cdot>x = \<bottom>") (simp_all add: e1p1.e_p_below)
+ next
+ case (sinr y)
+ then show ?case by (cases "p2\<cdot>y = \<bottom>") (simp_all add: e2p2.e_p_below)
+ qed
qed
lemma deflation_ssum_map:
@@ -349,15 +380,27 @@
interpret d2: deflation d2 by fact
fix x
show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
- apply (induct x, simp)
- apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
- apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
- done
+ proof (induct x)
+ case bottom
+ then show ?case by simp
+ next
+ case (sinl x)
+ then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.idem)
+ next
+ case (sinr y)
+ then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.idem)
+ qed
show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
- apply (induct x, simp)
- apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
- apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
- done
+ proof (induct x)
+ case bottom
+ then show ?case by simp
+ next
+ case (sinl x)
+ then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.below)
+ next
+ case (sinr y)
+ then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.below)
+ qed
qed
lemma finite_deflation_ssum_map:
--- a/src/HOL/Library/Extended_Real.thy Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Sat Jun 02 22:57:44 2018 +0100
@@ -627,9 +627,10 @@
"real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
by (cases y) auto
-(*To help with inferences like a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y,
+text \<open>
+ To help with inferences like \<^prop>\<open>a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y\<close>,
where x and y are real.
-*)
+\<close>
lemma le_ereal_le: "a \<le> ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a \<le> ereal y"
using ereal_less_eq(3) order.trans by blast
--- a/src/HOL/Library/Lub_Glb.thy Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/Library/Lub_Glb.thy Sat Jun 02 22:57:44 2018 +0100
@@ -221,7 +221,7 @@
lemma isLub_mono_imp_LIMSEQ:
fixes X :: "nat \<Rightarrow> real"
- assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+ assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use \<open>range X\<close> *)
assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
shows "X \<longlonglongrightarrow> u"
proof -
--- a/src/Pure/Concurrent/task_queue.ML Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Sat Jun 02 22:57:44 2018 +0100
@@ -21,6 +21,7 @@
val group_of_task: task -> group
val name_of_task: task -> string
val pri_of_task: task -> int
+ val eq_task: task * task -> bool
val str_of_task: task -> string
val str_of_task_groups: task -> string
val task_statistics: task -> Properties.T
@@ -129,8 +130,11 @@
fun group_of_task (Task {group, ...}) = group;
fun name_of_task (Task {name, ...}) = name;
+fun id_of_task (Task {id, ...}) = id;
fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
+fun eq_task (task1, task2) = id_of_task task1 = id_of_task task2;
+
fun str_of_task (Task {name, id, ...}) =
if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
--- a/src/Pure/Isar/class.ML Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Isar/class.ML Sat Jun 02 22:57:44 2018 +0100
@@ -375,12 +375,11 @@
in (type_params, dangling_term_params) end;
fun global_def (b, eq) thy =
- thy
- |> Thm.add_def_global false false (b, eq)
- |>> (Thm.varifyT_global o snd)
- |-> (fn def_thm => Global_Theory.store_thm (b, def_thm)
- #> snd
- #> pair def_thm);
+ let
+ val ((_, def_thm), thy') = thy |> Thm.add_def_global false false (b, eq);
+ val def_thm' = def_thm |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 |> Thm.varifyT_global;
+ val (_, thy'') = thy' |> Global_Theory.store_thm (b, def_thm');
+ in (def_thm', thy'') end;
fun canonical_const class phi dangling_params ((b, mx), rhs) thy =
let
--- a/src/Pure/PIDE/command.ML Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/PIDE/command.ML Sat Jun 02 22:57:44 2018 +0100
@@ -22,10 +22,10 @@
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
+ type print_fn = Toplevel.transition -> Toplevel.state -> unit
+ val print0: {pri: int, print_fn: print_fn} -> 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
type print_function =
{keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
{delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
@@ -342,9 +342,9 @@
in
-fun print0 e =
+fun print0 {pri, print_fn} =
make_print ("", [serial_string ()])
- {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
+ {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
fun print command_visible command_overlays keywords command_name eval old_prints =
let
--- a/src/Pure/PIDE/document.ML Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/PIDE/document.ML Sat Jun 02 22:57:44 2018 +0100
@@ -497,7 +497,8 @@
if Symtab.defined required name orelse visible_node node orelse pending_result node then
let
fun body () =
- (if forall finished_import deps then
+ (Execution.worker_task_active true;
+ if forall finished_import deps then
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
SOME exec =>
@@ -505,13 +506,19 @@
then SOME (Command.exec execution_id exec)
else NONE
| NONE => NONE)) node ()
- else ())
- handle exn => (Output.system_message (Runtime.exn_message exn); Exn.reraise exn);
+ else ();
+ Execution.worker_task_active false)
+ handle exn =>
+ (Output.system_message (Runtime.exn_message exn);
+ Execution.worker_task_active false;
+ Exn.reraise exn);
val future =
(singleton o Future.forks)
{name = "theory:" ^ name,
group = SOME (Future.new_group NONE),
- deps = Future.task_of delay_request' :: maps (the_list o #2 o #2) deps,
+ deps =
+ Future.task_of delay_request' :: Execution.active_tasks name @
+ maps (the_list o #2 o #2) deps,
pri = 0, interrupts = false} body;
in (node, SOME (Future.task_of future)) end
else (node, NONE));
@@ -707,17 +714,20 @@
adjust_pos = Position.adjust_offsets adjust,
segments = segments};
in
- fn () =>
+ fn _ =>
(Thy_Info.apply_presentation presentation_context thy;
commit_consolidated node)
end
- else fn () => commit_consolidated node;
+ 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)));
+ let
+ val print = eval |> Command.print0
+ {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
+ in (result_id, SOME (eval, print :: prints)) end);
val assign_update' = assign_update |> assign_update_change result_entry;
val node' = node |> assign_entry result_entry;
--- a/src/Pure/PIDE/execution.ML Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/PIDE/execution.ML Sat Jun 02 22:57:44 2018 +0100
@@ -10,6 +10,8 @@
val start: unit -> Document_ID.execution
val discontinue: unit -> unit
val is_running: Document_ID.execution -> bool
+ val active_tasks: string -> Future.task list
+ val worker_task_active: bool -> string -> unit
val is_running_exec: Document_ID.exec -> bool
val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
val snapshot: Document_ID.exec list -> Future.task list
@@ -31,17 +33,35 @@
(* global state *)
type print = {name: string, pri: int, body: unit -> unit};
-type exec_state = Future.group list * print list; (*active forks, prints*)
-type state =
- Document_ID.execution * (*overall document execution*)
- exec_state Inttab.table; (*running command execs*)
+type execs = (Future.group list * print list) (*active forks, prints*) Inttab.table;
+val init_execs: execs = Inttab.make [(Document_ID.none, ([], []))];
+
+datatype state =
+ State of
+ {execution_id: Document_ID.execution, (*overall document execution*)
+ nodes: Future.task list Symtab.table, (*active nodes*)
+ execs: execs}; (*running command execs*)
+
+fun make_state (execution_id, nodes, execs) =
+ State {execution_id = execution_id, nodes = nodes, execs = execs};
-val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
-val state = Synchronized.var "Execution.state" init_state;
+local
+ val state =
+ Synchronized.var "Execution.state" (make_state (Document_ID.none, Symtab.empty, init_execs));
+in
+
+fun get_state () = let val State args = Synchronized.value state in args end;
-fun get_state () = Synchronized.value state;
-fun change_state_result f = Synchronized.change_result state f;
-fun change_state f = Synchronized.change state f;
+fun change_state_result f =
+ Synchronized.change_result state (fn (State {execution_id, nodes, execs}) =>
+ let val (result, args') = f (execution_id, nodes, execs)
+ in (result, make_state args') end);
+
+fun change_state f =
+ Synchronized.change state (fn (State {execution_id, nodes, execs}) =>
+ make_state (f (execution_id, nodes, execs)));
+
+end;
fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
@@ -51,36 +71,52 @@
fun start () =
let
val execution_id = Document_ID.make ();
- val _ = change_state (apfst (K execution_id));
+ val _ = change_state (fn (_, nodes, execs) => (execution_id, nodes, execs));
in execution_id end;
-fun discontinue () = change_state (apfst (K Document_ID.none));
+fun discontinue () =
+ change_state (fn (_, nodes, execs) => (Document_ID.none, nodes, execs));
+
+fun is_running execution_id =
+ execution_id = #execution_id (get_state ());
+
+
+(* active nodes *)
-fun is_running execution_id = execution_id = #1 (get_state ());
+fun active_tasks node_name =
+ Symtab.lookup_list (#nodes (get_state ())) node_name;
+
+fun worker_task_active insert node_name =
+ change_state (fn (execution_id, nodes, execs) =>
+ let
+ val nodes' = nodes
+ |> (if insert then Symtab.insert_list else Symtab.remove_list)
+ Task_Queue.eq_task (node_name, the (Future.worker_task ()));
+ in (execution_id, nodes', execs) end);
(* running execs *)
fun is_running_exec exec_id =
- Inttab.defined (#2 (get_state ())) exec_id;
+ Inttab.defined (#execs (get_state ())) exec_id;
fun running execution_id exec_id groups =
- change_state_result (fn (execution_id', execs) =>
+ change_state_result (fn (execution_id', nodes, execs) =>
let
val ok = execution_id = execution_id' andalso not (Inttab.defined execs exec_id);
val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
- in (ok, (execution_id', execs')) end);
+ in (ok, (execution_id', nodes, execs')) end);
(* exec groups and tasks *)
-fun exec_groups ((_, execs): state) exec_id =
+fun exec_groups (execs: execs) exec_id =
(case Inttab.lookup execs exec_id of
SOME (groups, _) => groups
| NONE => []);
fun snapshot exec_ids =
- change_state_result (`(fn state => Future.snapshot (maps (exec_groups state) exec_ids)));
+ change_state_result (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
fun join exec_ids =
(case snapshot exec_ids of
@@ -91,7 +127,7 @@
deps = tasks, pri = 0, interrupts = false} I
|> Future.join; join exec_ids));
-fun peek exec_id = exec_groups (get_state ()) exec_id;
+fun peek exec_id = exec_groups (#execs (get_state ())) exec_id;
fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
@@ -112,11 +148,12 @@
let
val exec_id = the_default 0 (Position.parse_id pos);
val group = Future.worker_subgroup ();
- val _ = change_state (apsnd (fn execs =>
+ val _ = change_state (fn (execution_id, nodes, execs) =>
(case Inttab.lookup execs exec_id of
SOME (groups, prints) =>
- Inttab.update (exec_id, (group :: groups, prints)) execs
- | NONE => raise Fail (unregistered exec_id))));
+ let val execs' = Inttab.update (exec_id, (group :: groups, prints)) execs
+ in (execution_id, nodes, execs') end
+ | NONE => raise Fail (unregistered exec_id)));
val future =
(singleton o Future.forks)
@@ -149,18 +186,20 @@
(* print *)
fun print ({name, pos, pri}: params) e =
- change_state (apsnd (fn execs =>
+ change_state (fn (execution_id, nodes, execs) =>
let
val exec_id = the_default 0 (Position.parse_id pos);
val print = {name = name, pri = pri, body = e};
in
(case Inttab.lookup execs exec_id of
- SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs
+ SOME (groups, prints) =>
+ let val execs' = Inttab.update (exec_id, (groups, print :: prints)) execs
+ in (execution_id, nodes, execs') end
| NONE => raise Fail (unregistered exec_id))
- end));
+ end);
fun fork_prints exec_id =
- (case Inttab.lookup (#2 (get_state ())) exec_id of
+ (case Inttab.lookup (#execs (get_state ())) exec_id of
SOME (_, prints) =>
if Future.relevant prints then
let val pos = Position.thread_data () in
@@ -174,7 +213,7 @@
(* cleanup *)
fun purge exec_ids =
- (change_state o apsnd) (fn execs =>
+ change_state (fn (execution_id, nodes, execs) =>
let
val execs' = fold Inttab.delete_safe exec_ids execs;
val () =
@@ -183,12 +222,12 @@
else groups |> List.app (fn group =>
if Task_Queue.is_canceled group then ()
else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
- in execs' end);
+ in (execution_id, nodes, execs') end);
fun reset () =
- change_state_result (fn (_, execs) =>
+ change_state_result (fn (_, _, execs) =>
let val groups = Inttab.fold (append o #1 o #2) execs []
- in (groups, init_state) end);
+ in (groups, (Document_ID.none, Symtab.empty, init_execs)) end);
fun shutdown () =
(Future.shutdown ();
@@ -197,4 +236,3 @@
| exns => raise Par_Exn.make exns));
end;
-
--- a/src/Pure/Thy/export_theory.scala Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala Sat Jun 02 22:57:44 2018 +0100
@@ -60,6 +60,8 @@
/** theory content **/
+ val export_prefix: String = "theory/"
+
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
consts: List[Const],
@@ -100,7 +102,7 @@
cache: Option[Term.Cache] = None): Theory =
{
val parents =
- Export.read_entry(db, session_name, theory_name, "theory/parents") match {
+ Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
case Some(entry) => split_lines(entry.uncompressed().text)
case None =>
error("Missing theory export in session " + quote(session_name) + ": " +
@@ -147,7 +149,7 @@
def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
export_name: String, decode: XML.Body => List[A]): List[A] =
{
- Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
+ Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
case Some(entry) => decode(entry.uncompressed_yxml())
case None => Nil
}
--- a/src/Pure/Tools/dump.scala Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Tools/dump.scala Sat Jun 02 22:57:44 2018 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/dump.scala
Author: Makarius
-Dump build database produced by PIDE session.
+Dump cumulative PIDE session database.
*/
package isabelle
@@ -12,43 +12,68 @@
/* aspects */
sealed case class Aspect_Args(
- options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result)
+ options: Options,
+ progress: Progress,
+ output_dir: Path,
+ deps: Sessions.Deps,
+ result: Thy_Resources.Theories_Result)
{
- def write(node_name: Document.Node.Name, file_name: String, bytes: Bytes)
+ def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes)
{
- val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name)
+ val path = output_dir + Path.basic(node_name.theory) + file_name
Isabelle_System.mkdirs(path.dir)
Bytes.write(path, bytes)
}
- def write(node_name: Document.Node.Name, file_name: String, text: String): Unit =
+ def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit =
write(node_name, file_name, Bytes(text))
- def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit =
+ def write(node_name: Document.Node.Name, file_name: Path, 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)
+ sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
+ options: List[String] = Nil)
+ {
+ override def toString: String = name
+ }
- private val known_aspects =
+ val known_aspects =
List(
Aspect("messages", "output messages (YXML format)",
{ case args =>
for (node_name <- args.result.node_names) {
- args.write(node_name, "messages.yxml",
+ args.write(node_name, Path.explode("messages.yxml"),
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", args.result.markup_to_XML(node_name))
+ args.write(node_name, Path.explode("markup.yxml"),
+ args.result.markup_to_XML(node_name))
}
- })
- )
+ }),
+ Aspect("latex", "generated LaTeX source",
+ { case args =>
+ for {
+ node_name <- args.result.node_names
+ entry <- args.result.exports(node_name)
+ if entry.name == "document.tex"
+ } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+ }, options = List("editor_presentation")),
+ Aspect("theory", "foundational theory content",
+ { case args =>
+ for {
+ node_name <- args.result.node_names
+ entry <- args.result.exports(node_name)
+ if entry.name.startsWith(Export_Theory.export_prefix)
+ } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+ }, options = List("editor_presentation", "export_theory"))
+ ).sortBy(_.name)
def show_aspects: String =
- cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description))
+ cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
def the_aspect(name: String): Aspect =
known_aspects.find(aspect => aspect.name == name) getOrElse
@@ -73,7 +98,9 @@
if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
system_mode = system_mode) != 0) error(logic + " FAILED")
- val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
+ val dump_options =
+ (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
+ { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
/* dependencies */
@@ -102,7 +129,7 @@
/* dump aspects */
- val aspect_args = Aspect_Args(dump_options, progress, output_dir, theories_result)
+ val aspect_args = Aspect_Args(dump_options, progress, output_dir, deps, theories_result)
aspects.foreach(_.operation(aspect_args))
session_result
@@ -112,9 +139,9 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
+ Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
{
- var aspects: List[Aspect] = Nil
+ var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var output_dir = default_output_dir
@@ -133,7 +160,7 @@
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
Options are:
- -A NAMES dump named aspects (comma-separated list, see below)
+ -A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: """ + default_output_dir + """)
@@ -148,8 +175,7 @@
-v verbose
-x NAME exclude session NAME and all descendants
- Dump build database produced by PIDE session. The following dump aspects
- are known (option -A):
+ Dump cumulative PIDE session database, with the following aspects:
""" + Library.prefix_lines(" ", show_aspects) + "\n",
"A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),