--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Sep 02 16:20:09 2011 +0200
@@ -5,7 +5,7 @@
val tests = ["Brackin", "Instructions", "SML", "Verilog"];
-timing := true;
+Toplevel.timing := true;
warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
use_thys tests;
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/Admin/Benchmarks/HOL-record/ROOT.ML Fri Sep 02 16:20:09 2011 +0200
@@ -3,9 +3,9 @@
Some benchmark on large record.
*)
-val tests = ["RecordBenchmark"];
+val tests = ["Record_Benchmark"];
-timing := true;
+Toplevel.timing := true;
warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
use_thys tests;
--- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Fri Sep 02 14:43:20 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,395 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-record/RecordBenchmark.thy
- Author: Norbert Schirmer, DFKI
-*)
-
-header {* Benchmark for large record *}
-
-theory RecordBenchmark
-imports Main
-begin
-
-ML {* Record.timing := true *}
-
-record many_A =
-A000::nat
-A001::nat
-A002::nat
-A003::nat
-A004::nat
-A005::nat
-A006::nat
-A007::nat
-A008::nat
-A009::nat
-A010::nat
-A011::nat
-A012::nat
-A013::nat
-A014::nat
-A015::nat
-A016::nat
-A017::nat
-A018::nat
-A019::nat
-A020::nat
-A021::nat
-A022::nat
-A023::nat
-A024::nat
-A025::nat
-A026::nat
-A027::nat
-A028::nat
-A029::nat
-A030::nat
-A031::nat
-A032::nat
-A033::nat
-A034::nat
-A035::nat
-A036::nat
-A037::nat
-A038::nat
-A039::nat
-A040::nat
-A041::nat
-A042::nat
-A043::nat
-A044::nat
-A045::nat
-A046::nat
-A047::nat
-A048::nat
-A049::nat
-A050::nat
-A051::nat
-A052::nat
-A053::nat
-A054::nat
-A055::nat
-A056::nat
-A057::nat
-A058::nat
-A059::nat
-A060::nat
-A061::nat
-A062::nat
-A063::nat
-A064::nat
-A065::nat
-A066::nat
-A067::nat
-A068::nat
-A069::nat
-A070::nat
-A071::nat
-A072::nat
-A073::nat
-A074::nat
-A075::nat
-A076::nat
-A077::nat
-A078::nat
-A079::nat
-A080::nat
-A081::nat
-A082::nat
-A083::nat
-A084::nat
-A085::nat
-A086::nat
-A087::nat
-A088::nat
-A089::nat
-A090::nat
-A091::nat
-A092::nat
-A093::nat
-A094::nat
-A095::nat
-A096::nat
-A097::nat
-A098::nat
-A099::nat
-A100::nat
-A101::nat
-A102::nat
-A103::nat
-A104::nat
-A105::nat
-A106::nat
-A107::nat
-A108::nat
-A109::nat
-A110::nat
-A111::nat
-A112::nat
-A113::nat
-A114::nat
-A115::nat
-A116::nat
-A117::nat
-A118::nat
-A119::nat
-A120::nat
-A121::nat
-A122::nat
-A123::nat
-A124::nat
-A125::nat
-A126::nat
-A127::nat
-A128::nat
-A129::nat
-A130::nat
-A131::nat
-A132::nat
-A133::nat
-A134::nat
-A135::nat
-A136::nat
-A137::nat
-A138::nat
-A139::nat
-A140::nat
-A141::nat
-A142::nat
-A143::nat
-A144::nat
-A145::nat
-A146::nat
-A147::nat
-A148::nat
-A149::nat
-A150::nat
-A151::nat
-A152::nat
-A153::nat
-A154::nat
-A155::nat
-A156::nat
-A157::nat
-A158::nat
-A159::nat
-A160::nat
-A161::nat
-A162::nat
-A163::nat
-A164::nat
-A165::nat
-A166::nat
-A167::nat
-A168::nat
-A169::nat
-A170::nat
-A171::nat
-A172::nat
-A173::nat
-A174::nat
-A175::nat
-A176::nat
-A177::nat
-A178::nat
-A179::nat
-A180::nat
-A181::nat
-A182::nat
-A183::nat
-A184::nat
-A185::nat
-A186::nat
-A187::nat
-A188::nat
-A189::nat
-A190::nat
-A191::nat
-A192::nat
-A193::nat
-A194::nat
-A195::nat
-A196::nat
-A197::nat
-A198::nat
-A199::nat
-A200::nat
-A201::nat
-A202::nat
-A203::nat
-A204::nat
-A205::nat
-A206::nat
-A207::nat
-A208::nat
-A209::nat
-A210::nat
-A211::nat
-A212::nat
-A213::nat
-A214::nat
-A215::nat
-A216::nat
-A217::nat
-A218::nat
-A219::nat
-A220::nat
-A221::nat
-A222::nat
-A223::nat
-A224::nat
-A225::nat
-A226::nat
-A227::nat
-A228::nat
-A229::nat
-A230::nat
-A231::nat
-A232::nat
-A233::nat
-A234::nat
-A235::nat
-A236::nat
-A237::nat
-A238::nat
-A239::nat
-A240::nat
-A241::nat
-A242::nat
-A243::nat
-A244::nat
-A245::nat
-A246::nat
-A247::nat
-A248::nat
-A249::nat
-A250::nat
-A251::nat
-A252::nat
-A253::nat
-A254::nat
-A255::nat
-A256::nat
-A257::nat
-A258::nat
-A259::nat
-A260::nat
-A261::nat
-A262::nat
-A263::nat
-A264::nat
-A265::nat
-A266::nat
-A267::nat
-A268::nat
-A269::nat
-A270::nat
-A271::nat
-A272::nat
-A273::nat
-A274::nat
-A275::nat
-A276::nat
-A277::nat
-A278::nat
-A279::nat
-A280::nat
-A281::nat
-A282::nat
-A283::nat
-A284::nat
-A285::nat
-A286::nat
-A287::nat
-A288::nat
-A289::nat
-A290::nat
-A291::nat
-A292::nat
-A293::nat
-A294::nat
-A295::nat
-A296::nat
-A297::nat
-A298::nat
-A299::nat
-
-lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
-by simp
-
-lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
-by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_upd_simproc]) 1*})
-done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply simp
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
- apply auto
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-
-lemma True
-proof -
- {
- fix P r
- assume pre: "P (A155 r)"
- have "\<exists>x. P x"
- using pre
- apply -
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
- }
- show ?thesis ..
-qed
-
-
-lemma "\<exists>r. A155 r = x"
- apply (tactic {*simp_tac
- (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
- done
-
-
-end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Benchmarks/HOL-record/Record_Benchmark.thy Fri Sep 02 16:20:09 2011 +0200
@@ -0,0 +1,390 @@
+(* Title: Admin/Benchmarks/HOL-record/Record_Benchmark.thy
+ Author: Norbert Schirmer, DFKI
+*)
+
+header {* Benchmark for large record *}
+
+theory Record_Benchmark
+imports Main
+begin
+
+declare [[record_timing]]
+
+record many_A =
+A000::nat
+A001::nat
+A002::nat
+A003::nat
+A004::nat
+A005::nat
+A006::nat
+A007::nat
+A008::nat
+A009::nat
+A010::nat
+A011::nat
+A012::nat
+A013::nat
+A014::nat
+A015::nat
+A016::nat
+A017::nat
+A018::nat
+A019::nat
+A020::nat
+A021::nat
+A022::nat
+A023::nat
+A024::nat
+A025::nat
+A026::nat
+A027::nat
+A028::nat
+A029::nat
+A030::nat
+A031::nat
+A032::nat
+A033::nat
+A034::nat
+A035::nat
+A036::nat
+A037::nat
+A038::nat
+A039::nat
+A040::nat
+A041::nat
+A042::nat
+A043::nat
+A044::nat
+A045::nat
+A046::nat
+A047::nat
+A048::nat
+A049::nat
+A050::nat
+A051::nat
+A052::nat
+A053::nat
+A054::nat
+A055::nat
+A056::nat
+A057::nat
+A058::nat
+A059::nat
+A060::nat
+A061::nat
+A062::nat
+A063::nat
+A064::nat
+A065::nat
+A066::nat
+A067::nat
+A068::nat
+A069::nat
+A070::nat
+A071::nat
+A072::nat
+A073::nat
+A074::nat
+A075::nat
+A076::nat
+A077::nat
+A078::nat
+A079::nat
+A080::nat
+A081::nat
+A082::nat
+A083::nat
+A084::nat
+A085::nat
+A086::nat
+A087::nat
+A088::nat
+A089::nat
+A090::nat
+A091::nat
+A092::nat
+A093::nat
+A094::nat
+A095::nat
+A096::nat
+A097::nat
+A098::nat
+A099::nat
+A100::nat
+A101::nat
+A102::nat
+A103::nat
+A104::nat
+A105::nat
+A106::nat
+A107::nat
+A108::nat
+A109::nat
+A110::nat
+A111::nat
+A112::nat
+A113::nat
+A114::nat
+A115::nat
+A116::nat
+A117::nat
+A118::nat
+A119::nat
+A120::nat
+A121::nat
+A122::nat
+A123::nat
+A124::nat
+A125::nat
+A126::nat
+A127::nat
+A128::nat
+A129::nat
+A130::nat
+A131::nat
+A132::nat
+A133::nat
+A134::nat
+A135::nat
+A136::nat
+A137::nat
+A138::nat
+A139::nat
+A140::nat
+A141::nat
+A142::nat
+A143::nat
+A144::nat
+A145::nat
+A146::nat
+A147::nat
+A148::nat
+A149::nat
+A150::nat
+A151::nat
+A152::nat
+A153::nat
+A154::nat
+A155::nat
+A156::nat
+A157::nat
+A158::nat
+A159::nat
+A160::nat
+A161::nat
+A162::nat
+A163::nat
+A164::nat
+A165::nat
+A166::nat
+A167::nat
+A168::nat
+A169::nat
+A170::nat
+A171::nat
+A172::nat
+A173::nat
+A174::nat
+A175::nat
+A176::nat
+A177::nat
+A178::nat
+A179::nat
+A180::nat
+A181::nat
+A182::nat
+A183::nat
+A184::nat
+A185::nat
+A186::nat
+A187::nat
+A188::nat
+A189::nat
+A190::nat
+A191::nat
+A192::nat
+A193::nat
+A194::nat
+A195::nat
+A196::nat
+A197::nat
+A198::nat
+A199::nat
+A200::nat
+A201::nat
+A202::nat
+A203::nat
+A204::nat
+A205::nat
+A206::nat
+A207::nat
+A208::nat
+A209::nat
+A210::nat
+A211::nat
+A212::nat
+A213::nat
+A214::nat
+A215::nat
+A216::nat
+A217::nat
+A218::nat
+A219::nat
+A220::nat
+A221::nat
+A222::nat
+A223::nat
+A224::nat
+A225::nat
+A226::nat
+A227::nat
+A228::nat
+A229::nat
+A230::nat
+A231::nat
+A232::nat
+A233::nat
+A234::nat
+A235::nat
+A236::nat
+A237::nat
+A238::nat
+A239::nat
+A240::nat
+A241::nat
+A242::nat
+A243::nat
+A244::nat
+A245::nat
+A246::nat
+A247::nat
+A248::nat
+A249::nat
+A250::nat
+A251::nat
+A252::nat
+A253::nat
+A254::nat
+A255::nat
+A256::nat
+A257::nat
+A258::nat
+A259::nat
+A260::nat
+A261::nat
+A262::nat
+A263::nat
+A264::nat
+A265::nat
+A266::nat
+A267::nat
+A268::nat
+A269::nat
+A270::nat
+A271::nat
+A272::nat
+A273::nat
+A274::nat
+A275::nat
+A276::nat
+A277::nat
+A278::nat
+A279::nat
+A280::nat
+A281::nat
+A282::nat
+A283::nat
+A284::nat
+A285::nat
+A286::nat
+A287::nat
+A288::nat
+A289::nat
+A290::nat
+A291::nat
+A292::nat
+A293::nat
+A294::nat
+A295::nat
+A296::nat
+A297::nat
+A298::nat
+A299::nat
+
+lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
+ by simp
+
+lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply auto
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+
+lemma True
+proof -
+ {
+ fix P r
+ assume pre: "P (A155 r)"
+ have "\<exists>x. P x"
+ using pre
+ apply -
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+ }
+ show ?thesis ..
+qed
+
+
+lemma "\<exists>r. A155 r = x"
+ apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
+ done
+
+
+end
\ No newline at end of file
--- a/Admin/Benchmarks/IsaMakefile Fri Sep 02 14:43:20 2011 +0200
+++ b/Admin/Benchmarks/IsaMakefile Fri Sep 02 16:20:09 2011 +0200
@@ -33,7 +33,7 @@
HOL-record: HOL $(LOG)/HOL-record.gz
$(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML \
- HOL-record/RecordBenchmark.thy
+ HOL-record/Record_Benchmark.thy
@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
--- a/src/Pure/PIDE/document.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/Pure/PIDE/document.ML Fri Sep 02 16:20:09 2011 +0200
@@ -24,7 +24,7 @@
type edit = string * node_edit
type state
val init_state: state
- val define_command: command_id -> string -> state -> state
+ val define_command: command_id -> string -> string -> state -> state
val join_commands: state -> state
val cancel_execution: state -> Future.task list
val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
@@ -112,7 +112,13 @@
fun map_entries f =
map_node (fn (touched, header, perspective, entries, last_exec, result) =>
(touched, header, perspective, f entries, last_exec, result));
-fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
+fun get_entries (Node {entries, ...}) = entries;
+
+fun iterate_entries f = Entries.iterate NONE f o get_entries;
+fun iterate_entries_after start f (Node {entries, ...}) =
+ (case Entries.get_after entries start of
+ NONE => I
+ | SOME id => Entries.iterate (SOME id) f entries);
fun get_last_exec (Node {last_exec, ...}) = last_exec;
fun set_last_exec last_exec =
@@ -183,8 +189,9 @@
fun touch_node name nodes =
fold (fn desc =>
- update_node desc (set_touched true) #>
- desc <> name ? update_node desc (map_entries (reset_after NONE)))
+ update_node desc
+ (set_touched true #>
+ desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
(Graph.all_succs nodes [name]) nodes;
in
@@ -231,7 +238,7 @@
abstype state = State of
{versions: version Inttab.table, (*version_id -> document content*)
commands:
- Toplevel.transition future Inttab.table * (*command_id -> transition (future parsing)*)
+ (string * Toplevel.transition future) Inttab.table * (*command_id -> name * transition*)
Toplevel.transition future list, (*recent commands to be joined*)
execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
(*exec_id -> command_id with eval/print process*)
@@ -246,7 +253,7 @@
val init_state =
make_state (Inttab.make [(no_id, empty_version)],
- (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
+ (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
Future.new_group NONE);
@@ -267,7 +274,7 @@
(* commands *)
-fun define_command (id: command_id) text =
+fun define_command (id: command_id) name text =
map_state (fn (versions, (commands, recent), execs, execution) =>
let
val id_string = print_id id;
@@ -276,14 +283,14 @@
Position.setmp_thread_data (Position.id_only id_string)
(fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
val commands' =
- Inttab.update_new (id, tr) commands
+ Inttab.update_new (id, (name, tr)) commands
handle Inttab.DUP dup => err_dup "command" dup;
in (versions, (commands', tr :: recent), execs, execution) end);
fun the_command (State {commands, ...}) (id: command_id) =
(case Inttab.lookup (#1 commands) id of
NONE => err_undef "command" id
- | SOME tr => tr);
+ | SOME command => command);
val join_commands =
map_state (fn (versions, (commands, recent), execs, execution) =>
@@ -345,9 +352,7 @@
val _ = Multithreading.interrupted ();
val _ = Toplevel.status tr Markup.forked;
val start = Timing.start ();
- val (errs, result) =
- if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
- else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+ val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val _ = timing tr (Timing.result start);
val _ = Toplevel.status tr Markup.joined;
val _ = List.app (Toplevel.error_msg tr) errs;
@@ -384,28 +389,51 @@
local
-fun last_common last_visible node0 node =
+fun last_common state last_visible node0 node =
let
- fun get_common ((prev, id), exec) (found, (_, visible)) =
+ fun update_flags prev (visible, initial) =
+ let
+ val visible' = visible andalso prev <> last_visible;
+ val initial' = initial andalso
+ (case prev of
+ NONE => true
+ | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
+ in (visible', initial') end;
+ fun get_common ((prev, id), exec) (found, (_, flags)) =
if found then NONE
else
let val found' = is_none exec orelse exec <> lookup_entry node0 id
- in SOME (found', (prev, visible andalso prev <> last_visible)) end;
- in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
+ in SOME (found', (prev, update_flags prev flags)) end;
+ val (found, (common, flags)) =
+ iterate_entries get_common node (false, (NONE, (true, true)));
+ in
+ if found then (common, flags)
+ else
+ let val last = Entries.get_after (get_entries node) common
+ in (last, update_flags last flags) end
+ end;
+
+fun illegal_init () = error "Illegal theory header after end of theory";
-fun new_exec state init command_id' (execs, exec) =
- let
- val command' = the_command state command_id';
- val exec_id' = new_id ();
- val exec' =
- snd exec |> Lazy.map (fn (st, _) =>
- let val tr =
- Future.join command'
- |> Toplevel.modify_init init
- |> Toplevel.put_id (print_id exec_id');
- in run_command tr st end)
- |> pair command_id';
- in ((exec_id', exec') :: execs, exec') end;
+fun new_exec state bad_init command_id' (execs, exec, init) =
+ if bad_init andalso is_none init then NONE
+ else
+ let
+ val (name, tr0) = the_command state command_id';
+ val (modify_init, init') =
+ if Keyword.is_theory_begin name then
+ (Toplevel.modify_init (the_default illegal_init init), NONE)
+ else (I, init);
+ val exec_id' = new_id ();
+ val exec' =
+ snd exec |> Lazy.map (fn (st, _) =>
+ let val tr =
+ Future.join tr0
+ |> modify_init
+ |> Toplevel.put_id (print_id exec_id');
+ in run_command tr st end)
+ |> pair command_id';
+ in SOME ((exec_id', exec') :: execs, exec', init') end;
fun make_required nodes =
let
@@ -417,6 +445,10 @@
all_visible Symtab.empty;
in Symtab.defined required end;
+fun check_theory nodes name =
+ is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *)
+ is_some (Exn.get_res (get_header (get_node nodes name)));
+
fun init_theory deps name node =
let
val (thy_name, imports, uses) = Exn.release (get_header node);
@@ -454,6 +486,8 @@
let
val node0 = node_of old_version name;
fun init () = init_theory deps name node;
+ val bad_init =
+ not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
in
(singleton o Future.forks)
{name = "Document.update", group = NONE,
@@ -462,18 +496,19 @@
let
val required = is_required name;
val last_visible = #2 (get_perspective node);
- val (common, visible) = last_common last_visible node0 node;
+ val (common, (visible, initial)) = last_common state last_visible node0 node;
val common_exec = the_exec state (the_default_entry node common);
- val (execs, exec) = ([], common_exec) |>
+ val (execs, exec, _) =
+ ([], common_exec, if initial then SOME init else NONE) |>
(visible orelse required) ?
- iterate_entries (after_entry node common)
+ iterate_entries_after common
(fn ((prev, id), _) => fn res =>
if not required andalso prev = last_visible then NONE
- else SOME (new_exec state init id res)) node;
+ else new_exec state bad_init id res) node;
val no_execs =
- iterate_entries (after_entry node0 common)
+ iterate_entries_after common
(fn ((_, id0), exec0) => fn res =>
if is_none exec0 then NONE
else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
@@ -533,7 +568,7 @@
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
- (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
+ (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
in (versions, commands, execs, execution) end);
--- a/src/Pure/PIDE/document.scala Fri Sep 02 14:43:20 2011 +0200
+++ b/src/Pure/PIDE/document.scala Fri Sep 02 16:20:09 2011 +0200
@@ -47,6 +47,7 @@
case other: Name => node == other.node
case _ => false
}
+ override def toString: String = theory
}
sealed abstract class Edit[A, B]
--- a/src/Pure/PIDE/isar_document.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Fri Sep 02 16:20:09 2011 +0200
@@ -9,7 +9,8 @@
val _ =
Isabelle_Process.add_command "Isar_Document.define_command"
- (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
+ (fn [id, name, text] =>
+ Document.change_state (Document.define_command (Document.parse_id id) name text));
val _ =
Isabelle_Process.add_command "Isar_Document.cancel_execution"
--- a/src/Pure/PIDE/isar_document.scala Fri Sep 02 14:43:20 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Fri Sep 02 16:20:09 2011 +0200
@@ -148,8 +148,9 @@
{
/* commands */
- def define_command(id: Document.Command_ID, text: String): Unit =
- input("Isar_Document.define_command", Document.ID(id), text)
+ def define_command(command: Command): Unit =
+ input("Isar_Document.define_command",
+ Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
/* document versions */
--- a/src/Pure/System/session.scala Fri Sep 02 14:43:20 2011 +0200
+++ b/src/Pure/System/session.scala Fri Sep 02 16:20:09 2011 +0200
@@ -253,7 +253,7 @@
{
if (!global_state().defined_command(command.id)) {
global_state.change(_.define_command(command))
- prover.get.define_command(command.id, Symbol.encode(command.source))
+ prover.get.define_command(command)
}
}
doc_edits foreach {
--- a/src/Tools/jEdit/src/session_dockable.scala Fri Sep 02 14:43:20 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Fri Sep 02 16:20:09 2011 +0200
@@ -93,7 +93,8 @@
if (nodes_status != nodes_status1) {
nodes_status = nodes_status1
val order =
- Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
+ Library.sort_wrt((name: Document.Node.Name) => name.theory,
+ nodes_status.keySet.toList)
status.listData = order.map(name => name.theory + " " + nodes_status(name))
}
}