# HG changeset patch
# User huffman
# Date 1314202087 25200
# Node ID 9139a2a4c75a79d44a8e278919a9de36234432f0
# Parent  13e72da170fc21f642265243d0cca566d9427554# Parent  85103fbc9004b1c06c2f2a77a6eaed5e204cc87c
merged

diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Groups.thy	Wed Aug 24 09:08:07 2011 -0700
@@ -103,11 +103,6 @@
 
 hide_const (open) zero one
 
-syntax
-  "_index1"  :: index    ("\<^sub>1")
-translations
-  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
 lemma Let_0 [simp]: "Let 0 f = f 0"
   unfolding Let_def ..
 
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Library/Quotient_Set.thy	Wed Aug 24 09:08:07 2011 -0700
@@ -33,7 +33,7 @@
 lemma collect_rsp[quot_respect]:
   assumes "Quotient R Abs Rep"
   shows "((R ===> op =) ===> set_rel R) Collect Collect"
-  by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
+  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
 
 lemma collect_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
@@ -44,7 +44,7 @@
 lemma union_rsp[quot_respect]:
   assumes "Quotient R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
-  by (intro fun_relI) (auto simp add: set_rel_def)
+  by (intro fun_relI) (simp add: set_rel_def)
 
 lemma union_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
@@ -55,7 +55,7 @@
 lemma diff_rsp[quot_respect]:
   assumes "Quotient R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
-  by (intro fun_relI) (auto simp add: set_rel_def)
+  by (intro fun_relI) (simp add: set_rel_def)
 
 lemma diff_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
@@ -74,4 +74,13 @@
   unfolding fun_eq_iff
   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
 
+lemma mem_prs[quot_preserve]:
+  assumes "Quotient R Abs Rep"
+  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
+
+lemma mem_rsp[quot_respect]:
+  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
+  by (intro fun_relI) (simp add: set_rel_def)
+
 end
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -550,44 +550,53 @@
   end
 
 
-val e_override_params =
+fun e_override_params timeout =
   [("provers", "e"),
    ("max_relevant", "0"),
    ("type_enc", "poly_guards?"),
    ("sound", "true"),
-   ("slicing", "false")]
+   ("slicing", "false"),
+   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
 
-val vampire_override_params =
+fun vampire_override_params timeout =
   [("provers", "vampire"),
    ("max_relevant", "0"),
    ("type_enc", "poly_tags"),
    ("sound", "true"),
-   ("slicing", "false")]
+   ("slicing", "false"),
+   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
 
 fun run_reconstructor trivial full m name reconstructor named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
-    fun do_reconstructor thms ctxt =
-      (if !reconstructor = "sledgehammer_tac" then
-         (fn ctxt => fn thms =>
-            Method.insert_tac thms THEN'
-            (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-                 e_override_params
-             ORELSE'
-             Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-                 vampire_override_params))
-       else if !reconstructor = "smt" then
-         SMT_Solver.smt_tac
-       else if full orelse !reconstructor = "metis (full_types)" then
-         Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
-       else if !reconstructor = "metis (no_types)" then
-         Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
-       else if !reconstructor = "metis" then
-         Metis_Tactics.metis_tac []
-       else
-         K (K (K all_tac))) ctxt thms
-    fun apply_reconstructor thms =
-      Mirabelle.can_apply timeout (do_reconstructor thms) st
+    fun do_reconstructor named_thms ctxt =
+      let
+        val ref_of_str =
+          suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
+          #> fst
+        val thms = named_thms |> maps snd
+        val facts = named_thms |> map (ref_of_str o fst o fst)
+        val relevance_override = {add = facts, del = [], only = true}
+      in
+        if !reconstructor = "sledgehammer_tac" then
+          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+             (e_override_params timeout) relevance_override
+          ORELSE'
+          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+             (vampire_override_params timeout) relevance_override
+        else if !reconstructor = "smt" then
+          SMT_Solver.smt_tac ctxt thms
+        else if full orelse !reconstructor = "metis (full_types)" then
+          Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms
+        else if !reconstructor = "metis (no_types)" then
+          Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms
+        else if !reconstructor = "metis" then
+          Metis_Tactics.metis_tac [] ctxt thms
+        else
+          K all_tac
+      end
+    fun apply_reconstructor named_thms =
+      Mirabelle.can_apply timeout (do_reconstructor named_thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
       | with_time (true, t) = (change_data id (inc_reconstructor_success m);
@@ -599,8 +608,8 @@
           if name = "proof" then change_data id (inc_reconstructor_proofs m)
           else ();
           "succeeded (" ^ string_of_int t ^ ")")
-    fun timed_reconstructor thms =
-      (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)
+    fun timed_reconstructor named_thms =
+      (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
       handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
                ("timeout", false))
            | ERROR msg => ("error: " ^ msg, false)
@@ -610,7 +619,7 @@
     val _ = if trivial then ()
             else change_data id (inc_reconstructor_nontriv_calls m)
   in
-    maps snd named_thms
+    named_thms
     |> timed_reconstructor
     |>> log o prefix (reconstructor_tag reconstructor id)
     |> snd
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/TPTP/CASC_Setup.thy
--- a/src/HOL/TPTP/CASC_Setup.thy	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/TPTP/CASC_Setup.thy	Wed Aug 24 09:08:07 2011 -0700
@@ -119,14 +119,16 @@
    SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
-       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
+                      Sledgehammer_Filter.no_relevance_override))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
-       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
+                          Sledgehammer_Filter.no_relevance_override))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "metis"
        (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -1059,16 +1059,13 @@
     | formula => SOME formula
   end
 
-fun make_conjecture ctxt format type_enc ps =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val last = length ps - 1
-  in
-    map2 (fn j => fn ((name, loc), (kind, t)) =>
-             t |> make_formula thy type_enc (format <> CNF) name loc kind
-               |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
-         (0 upto last) ps
-  end
+fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not_trueprop t = s_not t
+
+fun make_conjecture thy format type_enc =
+  map (fn ((name, loc), (kind, t)) =>
+          t |> kind = Conjecture ? s_not_trueprop
+            |> make_formula thy type_enc (format <> CNF) name loc kind)
 
 (** Finite and infinite type inference **)
 
@@ -1552,7 +1549,7 @@
       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
-      map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
+      map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lambdas) =
       if preproc then
@@ -1563,7 +1560,7 @@
         |>> apfst (map (apsnd (apsnd freeze_term)))
       else
         ((conjs, facts), [])
-    val conjs = conjs |> make_conjecture ctxt format type_enc
+    val conjs = conjs |> make_conjecture thy format type_enc
     val (fact_names, facts) =
       facts
       |> map_filter (fn (name, (_, t)) =>
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -272,7 +272,7 @@
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
-   the conclusion variable to False. (Cf. "transform_elim_theorem" in
+   the conclusion variable to "False". (Cf. "transform_elim_theorem" in
    "Meson_Clausify".) *)
 fun transform_elim_prop t =
   case Logic.strip_imp_concl t of
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -38,6 +38,7 @@
   val trace : bool Config.T
   val ignore_no_atp : bool Config.T
   val instantiate_inducts : bool Config.T
+  val no_relevance_override : relevance_override
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
@@ -100,6 +101,8 @@
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
 
+val no_relevance_override = {add = [], del = [], only = false}
+
 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
 val abs_name = sledgehammer_prefix ^ "abs"
 val skolem_prefix = sledgehammer_prefix ^ "sko"
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -22,6 +22,7 @@
 open ATP_Systems
 open ATP_Translate
 open Sledgehammer_Util
+open Sledgehammer_Filter
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
 open Sledgehammer_Run
@@ -46,7 +47,6 @@
 
 (** Sledgehammer commands **)
 
-val no_relevance_override = {add = [], del = [], only = false}
 fun add_relevance_override ns : relevance_override =
   {add = ns, del = [], only = false}
 fun del_relevance_override ns : relevance_override =
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -57,16 +57,16 @@
           (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
            else "") ^ "...")
     val {goal, ...} = Proof.goal state
+    val facts =
+      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
        provers = provers, type_enc = type_enc, sound = true,
-       relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+       relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
        max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, slicing = false,
        timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
-    val facts =
-      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts, smt_filter = NONE}
diff -r 13e72da170fc -r 9139a2a4c75a src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -7,16 +7,22 @@
 
 signature SLEDGEHAMMER_TACTICS =
 sig
+  type relevance_override = Sledgehammer_Filter.relevance_override
+
   val sledgehammer_with_metis_tac :
-    Proof.context -> (string * string) list -> int -> tactic
+    Proof.context -> (string * string) list -> relevance_override -> int
+    -> tactic
   val sledgehammer_as_oracle_tac :
-    Proof.context -> (string * string) list -> int -> tactic
+    Proof.context -> (string * string) list -> relevance_override -> int
+    -> tactic
 end;
 
 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
 struct
 
-fun run_atp override_params i n ctxt goal =
+open Sledgehammer_Filter
+
+fun run_atp override_params relevance_override i n ctxt goal =
   let
     val chained_ths = [] (* a tactic has no chained ths *)
     val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
@@ -30,7 +36,6 @@
       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
     val relevance_fudge =
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
-    val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     val facts =
       Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
@@ -62,16 +67,17 @@
     |> Source.exhaust
   end
 
-fun sledgehammer_with_metis_tac ctxt override_params i th =
-  case run_atp override_params i i ctxt th of
+fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
+  case run_atp override_params relevance_override i i ctxt th of
     SOME facts =>
     Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
   | NONE => Seq.empty
 
-fun sledgehammer_as_oracle_tac ctxt override_params i th =
+fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
   let
     val thy = Proof_Context.theory_of ctxt
-    val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
+    val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
+                     i i ctxt th
   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
 
 end;
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/General/timing.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -20,6 +20,7 @@
   val start: unit -> start
   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
+  val is_relevant: timing -> bool
   val message: timing -> string
 end
 
@@ -67,11 +68,6 @@
 
 (* timing messages *)
 
-fun message {elapsed, cpu, gc} =
-  Time.toString elapsed ^ "s elapsed time, " ^
-  Time.toString cpu ^ "s cpu time, " ^
-  Time.toString gc ^ "s GC time" handle Time.Time => "";
-
 val min_time = Time.fromMilliseconds 1;
 
 fun is_relevant {elapsed, cpu, gc} =
@@ -79,6 +75,11 @@
   Time.>= (cpu, min_time) orelse
   Time.>= (gc, min_time);
 
+fun message {elapsed, cpu, gc} =
+  Time.toString elapsed ^ "s elapsed time, " ^
+  Time.toString cpu ^ "s cpu time, " ^
+  Time.toString gc ^ "s GC time" handle Time.Time => "";
+
 fun cond_timeit enabled msg e =
   if enabled then
     let
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/document.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -24,9 +24,10 @@
   type edit = string * node_edit
   type state
   val init_state: state
+  val define_command: command_id -> string -> state -> state
   val join_commands: state -> unit
   val cancel_execution: state -> Future.task list
-  val define_command: command_id -> string -> state -> state
+  val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
   val state: unit -> state
@@ -61,50 +62,62 @@
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
- {header: node_header,
+ {touched: bool,
+  header: node_header,
   perspective: perspective,
   entries: exec_id option Entries.T,  (*command entries with excecutions*)
   result: Toplevel.state lazy}
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (header, perspective, entries, result) =
-  Node {header = header, perspective = perspective, entries = entries, result = result};
+fun make_node (touched, header, perspective, entries, result) =
+  Node {touched = touched, header = header, perspective = perspective,
+    entries = entries, result = result};
 
-fun map_node f (Node {header, perspective, entries, result}) =
-  make_node (f (header, perspective, entries, result));
+fun map_node f (Node {touched, header, perspective, entries, result}) =
+  make_node (f (touched, header, perspective, entries, result));
 
-val no_perspective: perspective = (K false, []);
+fun make_perspective ids : perspective =
+  (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+
+val no_perspective = make_perspective [];
 val no_print = Lazy.value ();
 val no_result = Lazy.value Toplevel.toplevel;
 
 val empty_node =
-  make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
+  make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
 
 val clear_node =
-  map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result));
+  map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
 
 
 (* basic components *)
 
+fun is_touched (Node {touched, ...}) = touched;
+fun set_touched touched =
+  map_node (fn (_, header, perspective, entries, result) =>
+    (touched, header, perspective, entries, result));
+
 fun get_header (Node {header, ...}) = header;
 fun set_header header =
-  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+  map_node (fn (touched, _, perspective, entries, result) =>
+    (touched, header, perspective, entries, result));
 
 fun get_perspective (Node {perspective, ...}) = perspective;
-fun set_perspective perspective =
-  let val pred = Inttab.defined (Inttab.make (map (rpair ()) perspective)) in
-    map_node (fn (header, _, entries, result) => (header, (pred, perspective), entries, result))
-  end;
+fun set_perspective ids =
+  map_node (fn (touched, header, _, entries, result) =>
+    (touched, header, make_perspective ids, entries, result));
 
-fun map_entries f (Node {header, perspective, entries, result}) =
-  make_node (header, perspective, f entries, result);
+fun map_entries f =
+  map_node (fn (touched, header, perspective, entries, result) =>
+    (touched, header, perspective, f entries, result));
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
 
 fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
 fun set_result result =
-  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+  map_node (fn (touched, header, perspective, entries, _) =>
+    (touched, header, perspective, entries, result));
 
 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
 fun default_node name = Graph.default_node (name, empty_node);
@@ -146,35 +159,47 @@
 fun nodes_of (Version nodes) = nodes;
 val node_of = get_node o nodes_of;
 
+local
+
 fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
 
-fun touch_descendants name nodes =
-  fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
+fun touch_node name nodes =
+  fold (fn desc =>
+      update_node desc (set_touched true) #>
+      desc <> name ? update_node desc (map_entries (reset_after NONE)))
     (Graph.all_succs nodes [name]) nodes;
 
+in
+
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
-    (touch_descendants name
-      (case node_edit of
-        Clear => update_node name clear_node nodes
-      | Edits edits =>
-          nodes
-          |> update_node name (edit_node edits)
-      | Header header =>
-          let
-            val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
-            val nodes1 = nodes
-              |> default_node name
-              |> fold default_node parents;
-            val nodes2 = nodes1
-              |> Graph.Keys.fold
-                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
-            val (header', nodes3) =
-              (header, Graph.add_deps_acyclic (name, parents) nodes2)
-                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
-          in Graph.map_node name (set_header header') nodes3 end
-      | Perspective perspective =>
-          update_node name (set_perspective perspective) nodes));
+    (case node_edit of
+      Clear =>
+        nodes
+        |> update_node name clear_node
+        |> touch_node name
+    | Edits edits =>
+        nodes
+        |> update_node name (edit_node edits)
+        |> touch_node name
+    | Header header =>
+        let
+          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+          val nodes1 = nodes
+            |> default_node name
+            |> fold default_node parents;
+          val nodes2 = nodes1
+            |> Graph.Keys.fold
+                (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+          val (header', nodes3) =
+            (header, Graph.add_deps_acyclic (name, parents) nodes2)
+              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
+        in Graph.map_node name (set_header header') nodes3 end
+        |> touch_node name
+    | Perspective perspective =>
+        update_node name (set_perspective perspective) nodes);
+
+end;
 
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);
@@ -270,7 +295,8 @@
 
 local
 
-fun timing tr t = Toplevel.status tr (Markup.timing t);
+fun timing tr t =
+  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
 
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
@@ -320,6 +346,16 @@
 
 (** editing **)
 
+(* perspective *)
+
+fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
+  let
+    val old_version = the_version state old_id;
+    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
+    val new_version = edit_nodes (name, Perspective perspective) old_version;
+  in define_version new_id new_version state end;
+
+
 (* edit *)
 
 local
@@ -329,11 +365,32 @@
     NONE => true
   | SOME exec' => exec' <> exec);
 
-fun new_exec (command_id, command) (assigns, execs, exec) =
+fun init_theory deps name node =
   let
+    val (thy_name, imports, uses) = Exn.release (get_header node);
+    (* FIXME provide files via Scala layer *)
+    val (dir, files) =
+      if ML_System.platform_is_cygwin then (Path.current, [])
+      else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
+
+    val parents =
+      imports |> map (fn import =>
+        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
+          SOME thy => thy
+        | NONE =>
+            get_theory (Position.file_only import)
+              (#2 (Future.join (the (AList.lookup (op =) deps import))))));
+  in Thy_Load.begin_theory dir thy_name imports files parents end;
+
+fun new_exec state init command_id (assigns, execs, exec) =
+  let
+    val command = the_command state command_id;
     val exec_id' = new_id ();
     val exec' = exec |> Lazy.map (fn (st, _) =>
-      let val tr = Toplevel.put_id (print_id exec_id') (Future.join command)
+      let val tr =
+        Future.join command
+        |> Toplevel.modify_init init
+        |> Toplevel.put_id (print_id exec_id');
       in run_command tr st end);
   in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
 
@@ -348,46 +405,32 @@
     val updates =
       nodes_of new_version |> Graph.schedule
         (fn deps => fn (name, node) =>
-          (case first_entry NONE (is_changed (node_of old_version name)) node of
-            NONE => Future.value (([], [], []), node)
-          | SOME ((prev, id), _) =>
-              let
-                fun init () =
-                  let
-                    val (thy_name, imports, uses) = Exn.release (get_header node);
-                    (* FIXME provide files via Scala layer *)
-                    val (dir, files) =
-                      if ML_System.platform_is_cygwin then (Path.current, [])
-                      else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
-
-                    val parents =
-                      imports |> map (fn import =>
-                        (case Thy_Info.lookup_theory import of
-                          SOME thy => thy
-                        | NONE =>
-                            get_theory (Position.file_only import)
-                              (#2 (Future.join (the (AList.lookup (op =) deps import))))));
-                  in Thy_Load.begin_theory dir thy_name imports files parents end;
-                fun get_command id =
-                  (id, the_command state id |> Future.map (Toplevel.modify_init init));
-              in
-                (singleton o Future.forks)
-                  {name = "Document.edit", group = NONE,
-                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
-                  (fn () =>
-                    let
-                      val prev_exec =
-                        (case prev of
-                          NONE => no_id
-                        | SOME prev_id => the_default no_id (the_entry node prev_id));
-                      val (assigns, execs, last_exec) =
-                        fold_entries (SOME id) (new_exec o get_command o #2 o #1)
-                          node ([], [], #2 (the_exec state prev_exec));
-                      val node' = node
-                        |> fold update_entry assigns
-                        |> set_result (Lazy.map #1 last_exec);
-                    in ((assigns, execs, [(name, node')]), node') end)
-              end))
+          if not (is_touched node) then Future.value (([], [], []), node)
+          else
+            (case first_entry NONE (is_changed (node_of old_version name)) node of
+              NONE => Future.value (([], [], []), set_touched false node)
+            | SOME ((prev, id), _) =>
+                let
+                  fun init () = init_theory deps name node;
+                in
+                  (singleton o Future.forks)
+                    {name = "Document.edit", group = NONE,
+                      deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
+                    (fn () =>
+                      let
+                        val prev_exec =
+                          (case prev of
+                            NONE => no_id
+                          | SOME prev_id => the_default no_id (the_entry node prev_id));
+                        val (assigns, execs, last_exec) =
+                          fold_entries (SOME id) (new_exec state init o #2 o #1)
+                            node ([], [], #2 (the_exec state prev_exec));
+                        val node' = node
+                          |> fold update_entry assigns
+                          |> set_result (Lazy.map #1 last_exec)
+                          |> set_touched false;
+                      in ((assigns, execs, [(name, node')]), node') end)
+                end))
       |> Future.joins |> map #1;
 
     val state' = state
@@ -411,9 +454,8 @@
             let
               val (command_id, exec) = the_exec state exec_id;
               val (_, print) = Lazy.force exec;
-              val perspective = get_perspective node;
               val _ =
-                if #1 (get_perspective node) command_id orelse true  (* FIXME *)
+                if #1 (get_perspective node) command_id
                 then ignore (Lazy.future Future.default_params print)
                 else ();
             in () end;
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/document.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -54,11 +54,10 @@
     case class Header[A, B](header: Node_Header) extends Edit[A, B]
     case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
-    def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
-        : Header[A, B] =
+    def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
       header match {
-        case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
-        case exn => Header[A, B](exn)
+        case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
+        case exn => exn
       }
 
     val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
@@ -83,6 +82,9 @@
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {
+    def clear: Node = Node.empty.copy(header = header)
+
+
     /* commands */
 
     private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -146,7 +148,8 @@
     val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
   }
 
-  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
+  type Nodes = Map[String, Node]
+  sealed case class Version(val id: Version_ID, val nodes: Nodes)
 
 
   /* changes of plain text, eventually resulting in document edits */
@@ -221,8 +224,8 @@
 
   sealed case class State(
     val versions: Map[Version_ID, Version] = Map(),
-    val commands: Map[Command_ID, Command.State] = Map(),
-    val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
+    val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
+    val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
     val assignments: Map[Version_ID, State.Assignment] = Map(),
     val disposed: Set[ID] = Set(),  // FIXME unused!?
     val history: History = History.init)
@@ -248,15 +251,15 @@
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
-    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
+    def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment =
       assignments.getOrElse(version.id, fail)
 
     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
-        case Some((st, occs)) =>
+        case Some(st) =>
           val new_st = st.accumulate(message)
-          (new_st, copy(execs = execs + (id -> (new_st, occs))))
+          (new_st, copy(execs = execs + (id -> new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
@@ -269,14 +272,13 @@
     def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
     {
       val version = the_version(id)
-      val occs = Set(version)  // FIXME unused (!?)
 
       var new_execs = execs
       val assigned_execs =
         for ((cmd_id, exec_id) <- edits) yield {
           val st = the_command(cmd_id)
           if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
-          new_execs += (exec_id -> (st, occs))
+          new_execs += (exec_id -> st)
           (st.command, exec_id)
         }
       val new_assignment = the_assignment(version).assign(assigned_execs)
@@ -290,7 +292,14 @@
         case None => false
       }
 
-    def extend_history(previous: Future[Version],
+    def is_stable(change: Change): Boolean =
+      change.is_finished && is_assigned(change.version.get_finished)
+
+    def tip_stable: Boolean = is_stable(history.tip)
+    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+
+    def continue_history(
+        previous: Future[Version],
         edits: List[Edit_Text],
         version: Future[Version]): (Change, State) =
     {
@@ -302,11 +311,8 @@
     // persistent user-view
     def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
     {
-      val found_stable = history.undo_list.find(change =>
-        change.is_finished && is_assigned(change.version.get_finished))
-      require(found_stable.isDefined)
-      val stable = found_stable.get
-      val latest = history.undo_list.head
+      val stable = recent_stable.get
+      val latest = history.tip
 
       // FIXME proper treatment of removed nodes
       val edits =
@@ -323,7 +329,7 @@
         def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
 
         def state(command: Command): Command.State =
-          try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
+          try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
           catch { case _: State.Fail => command.empty_state }
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -12,6 +12,22 @@
     (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
 
 val _ =
+  Isabelle_Process.add_command "Isar_Document.update_perspective"
+    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
+      let
+        val old_id = Document.parse_id old_id_string;
+        val new_id = Document.parse_id new_id_string;
+        val ids = YXML.parse_body ids_yxml
+          |> let open XML.Decode in list int end;
+
+        val _ = Future.join_tasks (Document.cancel_execution state);
+      in
+        state
+        |> Document.update_perspective old_id new_id name ids
+        |> Document.execute new_id
+      end));
+
+val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
@@ -31,15 +47,15 @@
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
-      val running = Document.cancel_execution state;
-      val (updates, state') = Document.edit old_id new_id edits state;
-      val _ = Future.join_tasks running;
-      val _ = Document.join_commands state';
-      val _ =
-        Output.status (Markup.markup (Markup.assign new_id)
-          (implode (map (Markup.markup_only o Markup.edit) updates)));
-      val state'' = Document.execute new_id state';
-    in state'' end));
+        val running = Document.cancel_execution state;
+        val (updates, state') = Document.edit old_id new_id edits state;
+        val _ = Future.join_tasks running;
+        val _ = Document.join_commands state';
+        val _ =
+          Output.status (Markup.markup (Markup.assign new_id)
+            (implode (map (Markup.markup_only o Markup.edit) updates)));
+        val state'' = Document.execute new_id state';
+      in state'' end));
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.invoke_scala"
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -139,6 +139,17 @@
 
   /* document versions */
 
+  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
+    name: String, perspective: Command.Perspective)
+  {
+    val ids =
+    { import XML.Encode._
+      list(long)(perspective.map(_.id)) }
+
+    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
+      YXML.string_of_body(ids))
+  }
+
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
     edits: List[Document.Edit_Command])
   {
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/Syntax/syntax_trans.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -252,21 +252,22 @@
   if 1 <= i andalso i <= length structs then nth structs (i - 1)
   else error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
-fun struct_tr structs [Const ("_indexdefault", _)] =
-      Syntax.free (the_struct structs 1)
+fun legacy_struct structs i =
+  let
+    val x = the_struct structs i;
+    val _ =
+      legacy_feature
+        ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
+          Position.str_of (Position.thread_data ()) ^
+          " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+          (if i = 1 then " (may be omitted)" else ""))
+  in x end;
+
+fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
+  | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
   | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
       (case Lexicon.read_nat s of
-        SOME n =>
-          let
-            val x = the_struct structs n;
-            val advice =
-              " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
-              (if n = 1 then " (may be omitted)" else "");
-            val _ =
-              legacy_feature
-                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
-                  Position.str_of (Position.thread_data ()) ^ advice);
-          in Syntax.free x end
+        SOME i => Syntax.free (legacy_struct structs i)
       | NONE => raise TERM ("struct_tr", [t]))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/System/session.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -159,6 +159,28 @@
 
   val thy_info = new Thy_Info(thy_load)
 
+  def header_edit(name: String, master_dir: String,
+    header: Document.Node_Header): Document.Edit_Text =
+  {
+    def norm_import(s: String): String =
+    {
+      val thy_name = Thy_Header.base_name(s)
+      if (thy_load.is_loaded(thy_name)) thy_name
+      else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+    }
+    def norm_use(s: String): String =
+      file_store.append(master_dir, Path.explode(s))
+
+    val header1: Document.Node_Header =
+      header match {
+        case Exn.Res(Thy_Header(thy_name, _, _))
+        if (thy_load.is_loaded(thy_name)) =>
+          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
+        case _ => Document.Node.norm_header(norm_import, norm_use, header)
+      }
+    (name, Document.Node.Header(header1))
+  }
+
 
   /* actor messages */
 
@@ -180,6 +202,27 @@
     var prover: Option[Isabelle_Process with Isar_Document] = None
 
 
+    /* perspective */
+
+    def update_perspective(name: String, text_perspective: Text.Perspective)
+    {
+      val previous = global_state().history.tip.version.get_finished
+      val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
+
+      val text_edits: List[Document.Edit_Text] =
+        List((name, Document.Node.Perspective(text_perspective)))
+      val change =
+        global_state.change_yield(
+          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
+
+      val assignment = global_state().the_assignment(previous).get_finished
+      global_state.change(_.define_version(version, assignment))
+      global_state.change_yield(_.assign(version.id, Nil))
+
+      prover.get.update_perspective(previous.id, version.id, name, perspective)
+    }
+
+
     /* incoming edits */
 
     def handle_edits(name: String, master_dir: String,
@@ -189,20 +232,10 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
 
-      def norm_import(s: String): String =
-      {
-        val name = Thy_Header.base_name(s)
-        if (thy_load.is_loaded(name)) name
-        else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
-      }
-      def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
-      val norm_header =
-        Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header)
-
-      val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
+      val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
       val change =
-        global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
+        global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
 
       result.map {
         case (doc_edits, _) =>
@@ -213,6 +246,18 @@
     //}}}
 
 
+    /* exec state assignment */
+
+    def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+    //{{{
+    {
+      val cmds = global_state.change_yield(_.assign(id, edits))
+      for (cmd <- cmds) command_change_buffer ! cmd
+      assignments.event(Session.Assignment)
+    }
+    //}}}
+
+
     /* resulting changes */
 
     def handle_change(change: Change_Node)
@@ -292,11 +337,7 @@
           else if (result.is_status) {
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
-                try {
-                  val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
-                  for (cmd <- cmds) command_change_buffer ! cmd
-                  assignments.event(Session.Assignment)
-                }
+                try { handle_assign(id, edits) }
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -345,9 +386,11 @@
           reply(())
 
         case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
-          handle_edits(name, master_dir, header,
-            List(Document.Node.Edits(text_edits),
-              Document.Node.Perspective(perspective)))
+          if (text_edits.isEmpty && global_state().tip_stable)
+            update_perspective(name, perspective)
+          else
+            handle_edits(name, master_dir, header,
+              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
           reply(())
 
         case change: Change_Node if prover.isDefined =>
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -97,7 +97,7 @@
 
 
 
-  /** command perspective **/
+  /** perspective **/
 
   def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
   {
@@ -126,6 +126,26 @@
     }
   }
 
+  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
+    : (Command.Perspective, Option[Document.Nodes]) =
+  {
+    val node = nodes(name)
+    val perspective = command_perspective(node, text_perspective)
+    val new_nodes =
+      if (Command.equal_perspective(node.perspective, perspective)) None
+      else Some(nodes + (name -> node.copy(perspective = perspective)))
+    (perspective, new_nodes)
+  }
+
+  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
+    : (Command.Perspective, Document.Version) =
+  {
+    val nodes = previous.nodes
+    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
+    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
+    (perspective, version)
+  }
+
 
 
   /** text edits **/
@@ -212,7 +232,7 @@
       edits foreach {
         case (name, Document.Node.Clear()) =>
           doc_edits += (name -> Document.Node.Clear())
-          nodes -= name
+          nodes += (name -> nodes(name).clear)
 
         case (name, Document.Node.Edits(text_edits)) =>
           val node = nodes(name)
@@ -243,11 +263,11 @@
           }
 
         case (name, Document.Node.Perspective(text_perspective)) =>
-          val node = nodes(name)
-          val perspective = command_perspective(node, text_perspective)
-          if (!Command.equal_perspective(node.perspective, perspective)) {
-            doc_edits += (name -> Document.Node.Perspective(perspective))
-            nodes += (name -> node.copy(perspective = perspective))
+          update_perspective(nodes, name, text_perspective) match {
+            case (_, None) =>
+            case (perspective, Some(nodes1)) =>
+              doc_edits += (name -> Document.Node.Perspective(perspective))
+              nodes = nodes1
           }
       }
       (doc_edits.toList, Document.Version(Document.new_id(), nodes))
diff -r 13e72da170fc -r 9139a2a4c75a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/pure_thy.ML	Wed Aug 24 09:08:07 2011 -0700
@@ -127,6 +127,7 @@
     ("_strip_positions", typ "'a", NoSyn),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
     ("_constify",   typ "float_token => float_const",  Delimfix "_"),
+    ("_index1",     typ "index",                       Delimfix "\\<^sub>1"),
     ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
diff -r 13e72da170fc -r 9139a2a4c75a src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -87,16 +87,25 @@
   private object pending_edits  // owned by Swing thread
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
+    private var pending_perspective = false
+    private var last_perspective: Text.Perspective = Nil
+
     def snapshot(): List[Text.Edit] = pending.toList
 
     def flush()
     {
       Swing_Thread.require()
+
+      val new_perspective =
+        if (pending_perspective) { pending_perspective = false; perspective() }
+        else last_perspective
+
       snapshot() match {
-        case Nil =>
+        case Nil if new_perspective == last_perspective =>
         case edits =>
           pending.clear
-          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
+          last_perspective = new_perspective
+          session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
       }
     }
 
@@ -116,6 +125,18 @@
       pending += edit
       delay_flush()
     }
+
+    def update_perspective()
+    {
+      pending_perspective = true
+      delay_flush()
+    }
+  }
+
+  def update_perspective()
+  {
+    Swing_Thread.require()
+    pending_edits.update_perspective()
   }
 
 
diff -r 13e72da170fc -r 9139a2a4c75a src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -25,7 +25,8 @@
 import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
+  ScrollListener}
 import org.gjt.sp.jedit.syntax.{SyntaxStyle}
 
 
@@ -127,6 +128,16 @@
       yield Text.Range(start, stop))
   }
 
+  private def update_perspective = new TextAreaExtension
+  {
+    override def paintScreenLineRange(gfx: Graphics2D,
+      first_line: Int, last_line: Int, physical_lines: Array[Int],
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+    {
+      model.update_perspective()
+    }
+  }
+
 
   /* snapshot */
 
@@ -467,6 +478,7 @@
   private def activate()
   {
     val painter = text_area.getPainter
+    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
     text_area_painter.activate()
     text_area.getGutter.addExtension(gutter_painter)
@@ -492,6 +504,7 @@
     text_area.getGutter.removeExtension(gutter_painter)
     text_area_painter.deactivate()
     painter.removeExtension(tooltip_painter)
+    painter.removeExtension(update_perspective)
     exit_popup()
   }
 }
diff -r 13e72da170fc -r 9139a2a4c75a src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 24 09:08:07 2011 -0700
@@ -409,7 +409,7 @@
           Isabelle.start_session()
 
       case msg: BufferUpdate
-      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+      if msg.getWhat == BufferUpdate.LOADED =>
 
         val buffer = msg.getBuffer
         if (buffer != null && Isabelle.session.is_ready)