# HG changeset patch
# User wenzelm
# Date 1314973209 -7200
# Node ID 1cc7df9ff83bf17c93b7c3a3a59bc3ba45e60394
# Parent  5d6a11e166cfd05c55ee6809781d56801eedc11f# Parent  5938beb84adc6243ddf7c3bc1b9c9163438e09dd
merged

diff -r 5d6a11e166cf -r 1cc7df9ff83b Admin/Benchmarks/HOL-datatype/ROOT.ML
--- 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;
diff -r 5d6a11e166cf -r 1cc7df9ff83b Admin/Benchmarks/HOL-record/ROOT.ML
--- 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;
diff -r 5d6a11e166cf -r 1cc7df9ff83b Admin/Benchmarks/HOL-record/RecordBenchmark.thy
--- 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
diff -r 5d6a11e166cf -r 1cc7df9ff83b Admin/Benchmarks/HOL-record/Record_Benchmark.thy
--- /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
diff -r 5d6a11e166cf -r 1cc7df9ff83b Admin/Benchmarks/IsaMakefile
--- 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
 
 
diff -r 5d6a11e166cf -r 1cc7df9ff83b src/Pure/PIDE/document.ML
--- 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);
 
diff -r 5d6a11e166cf -r 1cc7df9ff83b src/Pure/PIDE/document.scala
--- 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]
diff -r 5d6a11e166cf -r 1cc7df9ff83b src/Pure/PIDE/isar_document.ML
--- 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"
diff -r 5d6a11e166cf -r 1cc7df9ff83b src/Pure/PIDE/isar_document.scala
--- 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 */
diff -r 5d6a11e166cf -r 1cc7df9ff83b src/Pure/System/session.scala
--- 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 {
diff -r 5d6a11e166cf -r 1cc7df9ff83b src/Tools/jEdit/src/session_dockable.scala
--- 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))
           }
       }