# HG changeset patch
# User wenzelm
# Date 1314112374 -7200
# Node ID 8d6869a8d4ec7a4551b12077ce9261749e2b9ed2
# Parent  867928fe20e930b504fdac46ffe7bcfc076ab523# Parent  a3b5fdfb04a3f0fd9dcd2bd0cdfac1403d5057de
merged

diff -r 867928fe20e9 -r 8d6869a8d4ec src/HOL/HOLCF/IOA/ABP/Check.ML
--- a/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -112,21 +112,21 @@
    ------------------------------------*)
 
 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
-  let fun prec x = (Output.raw_stdout ","; pre x)
+  let fun prec x = (Output.physical_stdout ","; pre x)
   in
     (case lll of
-      [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
-    | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
+      [] => (Output.physical_stdout lpar; Output.physical_stdout rpar)
+    | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar))
    end;
 
-fun pr_bool true = Output.raw_stdout "true"
-|   pr_bool false = Output.raw_stdout "false";
+fun pr_bool true = Output.physical_stdout "true"
+|   pr_bool false = Output.physical_stdout "false";
 
-fun pr_msg m = Output.raw_stdout "m"
-|   pr_msg n = Output.raw_stdout "n"
-|   pr_msg l = Output.raw_stdout "l";
+fun pr_msg m = Output.physical_stdout "m"
+|   pr_msg n = Output.physical_stdout "n"
+|   pr_msg l = Output.physical_stdout "l";
 
-fun pr_act a = Output.raw_stdout (case a of
+fun pr_act a = Output.physical_stdout (case a of
       Next => "Next"|                         
       S_msg(ma) => "S_msg(ma)"  |
       R_msg(ma) => "R_msg(ma)"  |
@@ -135,17 +135,17 @@
       S_ack(b)   => "S_ack(b)" |                      
       R_ack(b)   => "R_ack(b)");
 
-fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
+fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_stdout ">");
 
 val pr_bool_list  = print_list("[","]",pr_bool);
 val pr_msg_list   = print_list("[","]",pr_msg);
 val pr_pkt_list   = print_list("[","]",pr_pkt);
 
 fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
-        (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
-         pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
-         pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
-         pr_bool_list ch2; Output.raw_stdout "}");
+        (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p;  Output.physical_stdout ", ";
+         pr_bool a;  Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", ";
+         pr_bool b;  Output.physical_stdout ", "; pr_pkt_list ch1;  Output.physical_stdout ", ";
+         pr_bool_list ch2; Output.physical_stdout "}");
 
 
 
diff -r 867928fe20e9 -r 8d6869a8d4ec src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Aug 23 17:12:54 2011 +0200
@@ -72,7 +72,7 @@
   by (auto simp: Pi_def)
 
 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
-  by (auto intro: Pi_I)
+  by auto
 
 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
   by (simp add: Pi_def)
@@ -257,7 +257,7 @@
 where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
 
 lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
-unfolding extensional_def by (auto intro: ext)
+unfolding extensional_def by auto
 
 lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
 unfolding extensional_funcset_def by simp
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -51,12 +51,12 @@
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
-  val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> task list
   val cancel: 'a future -> task list
   type fork_params =
     {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
+  val default_params: fork_params
   val forks: fork_params -> (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
@@ -125,11 +125,6 @@
 fun peek x = Single_Assignment.peek (result_of x);
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished future evaluation");
-
 
 
 (** scheduling **)
@@ -467,6 +462,9 @@
 type fork_params =
   {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
 
+val default_params: fork_params =
+  {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
+
 fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
   if null es then []
   else
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -11,11 +11,12 @@
   type 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
   val is_finished: 'a lazy -> bool
-  val get_finished: 'a lazy -> 'a
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
+  val map: ('a -> 'b) -> 'a lazy -> 'b lazy
+  val future: Future.fork_params -> 'a lazy -> 'a future
 end;
 
 structure Lazy: LAZY =
@@ -40,11 +41,6 @@
 
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished lazy evaluation");
-
 
 (* force result *)
 
@@ -77,9 +73,19 @@
           | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
         end) ());
 
-fun force r = Exn.release (force_result r);
 
 end;
+
+fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+  if is_finished x then Future.value_result (force_result x)
+  else (singleton o Future.forks) params (fn () => force x);
+
 end;
 
 type 'a lazy = 'a Lazy.lazy;
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -27,11 +27,6 @@
 
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished lazy evaluation");
-
 
 (* force result *)
 
@@ -45,6 +40,14 @@
   in result end;
 
 fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+  if is_finished x then Future.value_result (force_result x)
+  else (singleton o Future.forks) params (fn () => force x);
 
 end;
 end;
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/General/output.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -22,9 +22,9 @@
   val output_width: string -> output * int
   val output: string -> output
   val escape: output -> string
-  val raw_stdout: output -> unit
-  val raw_stderr: output -> unit
-  val raw_writeln: output -> unit
+  val physical_stdout: output -> unit
+  val physical_stderr: output -> unit
+  val physical_writeln: output -> unit
   structure Private_Hooks:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
@@ -78,24 +78,24 @@
 
 (* raw output primitives -- not to be used in user-space *)
 
-fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
-fun raw_writeln "" = ()
-  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
+fun physical_writeln "" = ()
+  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
 
 
 (* Isabelle output channels *)
 
 structure Private_Hooks =
 struct
-  val writeln_fn = Unsynchronized.ref raw_writeln;
+  val writeln_fn = Unsynchronized.ref physical_writeln;
   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+  val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### ");
   val error_fn =
-    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
-  val prompt_fn = Unsynchronized.ref raw_stdout;
+    Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s)));
+  val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
   val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -84,6 +84,19 @@
 
   def span(toks: List[Token]): Command =
     new Command(Document.no_id, toks)
+
+
+  /* perspective */
+
+  type Perspective = List[Command]  // visible commands in canonical order
+
+  def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
+  {
+    require(p1.forall(_.is_defined))
+    require(p2.forall(_.is_defined))
+    p1.length == p2.length &&
+      (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+  }
 }
 
 
@@ -93,12 +106,12 @@
 {
   /* classification */
 
+  def is_defined: Boolean = id != Document.no_id
+
   def is_command: Boolean = !span.isEmpty && span.head.is_command
   def is_ignored: Boolean = span.forall(_.is_ignored)
   def is_malformed: Boolean = !is_command && !is_ignored
 
-  def is_unparsed = id == Document.no_id
-
   def name: String = if (is_command) span.head.content else ""
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -19,7 +19,8 @@
   datatype node_edit =
     Clear |
     Edits of (command_id option * command_id option) list |
-    Header of node_header
+    Header of node_header |
+    Perspective of command_id list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -56,34 +57,54 @@
 (** document structure **)
 
 type node_header = (string * string list * (string * bool) list) Exn.result;
+type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
  {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, entries, result) =
-  Node {header = header, entries = entries, result = result};
+fun make_node (header, perspective, entries, result) =
+  Node {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 {header, entries, result}) =
-  make_node (f (header, entries, result));
+val no_perspective: perspective = (K false, []);
+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);
+
+val clear_node =
+  map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result));
+
+
+(* basic components *)
 
 fun get_header (Node {header, ...}) = header;
-fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
+fun set_header header =
+  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
 
-fun map_entries f (Node {header, entries, result}) = make_node (header, f 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 map_entries f (Node {header, perspective, entries, result}) =
+  make_node (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.get_finished result);
-fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
-
-val empty_exec = Lazy.value Toplevel.toplevel;
-val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
-val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
+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));
 
 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);
@@ -95,7 +116,8 @@
 datatype node_edit =
   Clear |
   Edits of (command_id option * command_id option) list |
-  Header of node_header;
+  Header of node_header |
+  Perspective of command_id list;
 
 type edit = string * node_edit;
 
@@ -150,7 +172,9 @@
             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));
+          in Graph.map_node name (set_header header') nodes3 end
+      | Perspective perspective =>
+          update_node name (set_perspective perspective) nodes));
 
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);
@@ -164,7 +188,8 @@
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
-  execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
+  execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
+    (*exec_id -> command_id with eval/print process*)
   execution: Future.group}  (*global execution process*)
 with
 
@@ -177,7 +202,7 @@
 val init_state =
   make_state (Inttab.make [(no_id, empty_version)],
     Inttab.make [(no_id, Future.value Toplevel.empty)],
-    Inttab.make [(no_id, empty_exec)],
+    Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
     Future.new_group NONE);
 
 
@@ -252,14 +277,9 @@
     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   | NONE => ());
 
-fun async_state tr st =
-  (singleton o Future.forks)
-    {name = "Document.async_state", group = SOME (Future.new_group NONE),
-      deps = [], pri = 0, interrupts = true}
-    (fn () =>
-      Toplevel.setmp_thread_position tr
-        (fn () => Toplevel.print_state false st) ())
-  |> ignore;
+fun print_state tr st =
+  (Lazy.lazy o Toplevel.setmp_thread_position tr)
+    (fn () => Toplevel.print_state false st);
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -286,12 +306,11 @@
     val _ = List.app (Toplevel.error_msg tr) errs;
   in
     (case result of
-      NONE => (Toplevel.status tr Markup.failed; st)
+      NONE => (Toplevel.status tr Markup.failed; (st, no_print))
     | SOME st' =>
        (Toplevel.status tr Markup.finished;
         proof_status tr st';
-        if do_print then async_state tr st' else ();
-        st'))
+        (st', if do_print then print_state tr st' else no_print)))
   end;
 
 end;
@@ -313,13 +332,10 @@
 fun new_exec (command_id, command) (assigns, execs, exec) =
   let
     val exec_id' = new_id ();
-    val exec' =
-      Lazy.lazy (fn () =>
-        let
-          val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command);
-          val st = Lazy.get_finished exec;
-        in run_command tr st end);
-  in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;
+    val exec' = exec |> Lazy.map (fn (st, _) =>
+      let val tr = Toplevel.put_id (print_id exec_id') (Future.join command)
+      in run_command tr st end);
+  in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
 
 in
 
@@ -351,7 +367,7 @@
                         | 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
+                  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
@@ -364,12 +380,12 @@
                         (case prev of
                           NONE => no_id
                         | SOME prev_id => the_default no_id (the_entry node prev_id));
-                      val (assigns, execs, result) =
+                      val (assigns, execs, last_exec) =
                         fold_entries (SOME id) (new_exec o get_command o #2 o #1)
-                          node ([], [], the_exec state prev_exec);
+                          node ([], [], #2 (the_exec state prev_exec));
                       val node' = node
                         |> fold update_entry assigns
-                        |> set_result result;
+                        |> set_result (Lazy.map #1 last_exec);
                     in ((assigns, execs, [(name, node')]), node') end)
               end))
       |> Future.joins |> map #1;
@@ -390,8 +406,17 @@
     let
       val version = the_version state version_id;
 
-      fun force_exec NONE = ()
-        | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
+      fun force_exec _ NONE = ()
+        | force_exec node (SOME exec_id) =
+            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 *)
+                then ignore (Lazy.future Future.default_params print)
+                else ();
+            in () end;
 
       val execution = Future.new_group NONE;
       val _ =
@@ -400,7 +425,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 = true}
-              (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
+              (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node));
 
     in (versions, commands, execs, execution) end);
 
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -31,35 +31,37 @@
 
   /* named nodes -- development graph */
 
-  type Edit[A] = (String, Node.Edit[A])
-  type Edit_Text = Edit[Text.Edit]
-  type Edit_Command = Edit[(Option[Command], Option[Command])]
-  type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
+  type Edit[A, B] = (String, Node.Edit[A, B])
+  type Edit_Text = Edit[Text.Edit, Text.Perspective]
+  type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
 
   type Node_Header = Exn.Result[Thy_Header]
 
   object Node
   {
-    sealed abstract class Edit[A]
+    sealed abstract class Edit[A, B]
     {
-      def map[B](f: A => B): Edit[B] =
+      def foreach(f: A => Unit)
+      {
         this match {
-          case Clear() => Clear()
-          case Edits(es) => Edits(es.map(f))
-          case Header(header) => Header(header)
+          case Edits(es) => es.foreach(f)
+          case _ =>
         }
+      }
     }
-    case class Clear[A]() extends Edit[A]
-    case class Edits[A](edits: List[A]) extends Edit[A]
-    case class Header[A](header: Node_Header) extends Edit[A]
+    case class Clear[A, B]() extends Edit[A, B]
+    case class Edits[A, B](edits: List[A]) extends Edit[A, B]
+    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](f: String => String, g: String => String, header: Node_Header): Header[A] =
+    def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
+        : Header[A, B] =
       header match {
-        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
-        case exn => Header[A](exn)
+        case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
+        case exn => Header[A, B](exn)
       }
 
-    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
+    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -77,6 +79,7 @@
 
   sealed case class Node(
     val header: Node_Header,
+    val perspective: Command.Perspective,
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -27,7 +27,8 @@
                   fn ([], a) =>
                     Document.Header
                       (Exn.Res (triple string (list string) (list (pair string bool)) a)),
-                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
+                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+                  fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
       val running = Document.cancel_execution state;
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -140,18 +140,20 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-    edits: List[Document.Edit_Command_ID])
+    edits: List[Document.Edit_Command])
   {
     val edits_yxml =
     { import XML.Encode._
-      def encode: T[List[Document.Edit_Command_ID]] =
+      def id: T[Command] = (cmd => long(cmd.id))
+      def encode: T[List[Document.Edit_Command]] =
         list(pair(string,
           variant(List(
             { case Document.Node.Clear() => (Nil, Nil) },
-            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
+            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
             { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
                 (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
-            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
+            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
+            { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -22,10 +22,7 @@
     type Entry = (Text.Info[Any], Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
 
-    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
-      {
-        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
-      })
+    val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
 
     def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
     def single(entry: Entry): T = update(empty, entry)
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -8,6 +8,11 @@
 package isabelle
 
 
+import scala.collection.mutable
+import scala.math.Ordering
+import scala.util.Sorting
+
+
 object Text
 {
   /* offset */
@@ -20,6 +25,11 @@
   object Range
   {
     def apply(start: Offset): Range = Range(start, start)
+
+    object Ordering extends scala.math.Ordering[Text.Range]
+    {
+      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
+    }
   }
 
   sealed case class Range(val start: Offset, val stop: Offset)
@@ -50,6 +60,33 @@
   }
 
 
+  /* perspective */
+
+  type Perspective = List[Range]  // visible text partitioning in canonical order
+
+  def perspective(ranges: Seq[Range]): Perspective =
+  {
+    val sorted_ranges = ranges.toArray
+    Sorting.quickSort(sorted_ranges)(Range.Ordering)
+
+    val result = new mutable.ListBuffer[Text.Range]
+    var last: Option[Text.Range] = None
+    for (range <- sorted_ranges)
+    {
+      last match {
+        case Some(last_range)
+        if ((last_range overlaps range) || last_range.stop == range.start) =>
+          last = Some(Text.Range(last_range.start, range.stop))
+        case _ =>
+          result ++= last
+          last = Some(range)
+      }
+    }
+    result ++= last
+    result.toList
+  }
+
+
   /* information associated with text range */
 
   sealed case class Info[A](val range: Text.Range, val info: A)
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -75,7 +75,7 @@
 fun message bg en prfx text =
   (case render text of
     "" => ()
-  | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
+  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
  (Output.Private_Hooks.writeln_fn := message "" "" "";
@@ -85,7 +85,7 @@
   Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
   Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 fun panic s =
   (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -66,7 +66,7 @@
 
 fun matching_pgip_id id = (id = ! pgip_id)
 
-val output_xml_fn = Unsynchronized.ref Output.raw_writeln
+val output_xml_fn = Unsynchronized.ref Output.physical_writeln
 fun output_xml s = ! output_xml_fn (XML.string_of s);
 
 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -1009,7 +1009,7 @@
 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
 
 local
-    val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
+    val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
 in
 
 (* Set recipient for PGIP results *)
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -255,8 +255,19 @@
 fun struct_tr structs [Const ("_indexdefault", _)] =
       Syntax.free (the_struct structs 1)
   | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
-      Syntax.free (the_struct structs
-        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
+      (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
+      | NONE => raise TERM ("struct_tr", [t]))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
 
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -171,7 +171,7 @@
 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
-    val _ = Output.raw_stdout Symbol.STX;
+    val _ = Output.physical_stdout Symbol.STX;
 
     val _ = quick_and_dirty := true;
     val _ = Goal.parallel_proofs := 0;
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/System/session.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -107,7 +107,7 @@
           val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
             |> Real.fmt (StringCvt.FIX (SOME 2));
           val _ =
-            Output.raw_stderr ("Timing " ^ item ^ " (" ^
+            Output.physical_stderr ("Timing " ^ item ^ " (" ^
               string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
               Timing.message timing ^ ", factor " ^ factor ^ ")\n");
         in () end
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -164,10 +164,10 @@
 
   private case class Start(timeout: Time, args: List[String])
   private case object Interrupt
-  private case class Init_Node(
-    name: String, master_dir: String, header: Document.Node_Header, text: String)
-  private case class Edit_Node(
-    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
+  private case class Init_Node(name: String, master_dir: String,
+    header: Document.Node_Header, perspective: Text.Perspective, text: String)
+  private case class Edit_Node(name: String, master_dir: String,
+    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   private case class Change_Node(
     name: String,
     doc_edits: List[Document.Edit_Command],
@@ -183,7 +183,7 @@
     /* incoming edits */
 
     def handle_edits(name: String, master_dir: String,
-        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
+        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
     //{{{
     {
       val syntax = current_syntax()
@@ -196,7 +196,8 @@
         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](norm_import, norm_use, header)
+      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 result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
@@ -229,22 +230,20 @@
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
 
-      def id_command(command: Command): Document.Command_ID =
+      def id_command(command: Command)
       {
         if (global_state().lookup_command(command.id).isEmpty) {
           global_state.change(_.define_command(command))
           prover.get.define_command(command.id, Symbol.encode(command.source))
         }
-        command.id
       }
-      val id_edits =
-        doc_edits map {
-          case (name, edit) =>
-            (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }))
-        }
+      doc_edits foreach {
+        case (_, edit) =>
+          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+      }
 
       global_state.change(_.define_version(version, former_assignment))
-      prover.get.edit_version(previous.id, version.id, id_edits)
+      prover.get.edit_version(previous.id, version.id, doc_edits)
     }
     //}}}
 
@@ -337,14 +336,18 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
-        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
+        case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
           // FIXME compare with existing node
           handle_edits(name, master_dir, header,
-            List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
+            List(Document.Node.Clear(),
+              Document.Node.Edits(List(Text.Edit.insert(0, text))),
+              Document.Node.Perspective(perspective)))
           reply(())
 
-        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
-          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
+        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)))
           reply(())
 
         case change: Change_Node if prover.isDefined =>
@@ -372,9 +375,13 @@
 
   def interrupt() { session_actor ! Interrupt }
 
-  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
-  { session_actor !? Init_Node(name, master_dir, header, text) }
+  // FIXME simplify signature
+  def init_node(name: String, master_dir: String,
+    header: Document.Node_Header, perspective: Text.Perspective, text: String)
+  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
 
-  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, master_dir, header, edits) }
+  // FIXME simplify signature
+  def edit_node(name: String, master_dir: String, header: Document.Node_Header,
+    perspective: Text.Perspective, edits: List[Text.Edit])
+  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
 }
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/Thy/present.ML	Tue Aug 23 17:12:54 2011 +0200
@@ -289,7 +289,8 @@
       val documents =
         if doc = "" then []
         else if not (can File.check_dir document_path) then
-          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
+          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
+           else (); [])
         else read_variants doc_variants;
 
       val parent_index_path = Path.append Path.parent index_path;
@@ -403,14 +404,14 @@
         File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
         List.app finish_html thys;
         List.app (uncurry File.write) files;
-        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
         else ())
       else ();
 
     val _ =
       (case dump_prefix of NONE => () | SOME (cp, path) =>
        (prepare_sources cp path;
-        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
+        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
         else ()));
 
     val doc_paths =
@@ -421,7 +422,8 @@
         in isabelle_document true doc_format name tags path html_prefix end);
     val _ =
       if verbose then
-        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
+        doc_paths
+        |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
       else ();
   in
     browser_info := empty_browser_info;
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -97,6 +97,37 @@
 
 
 
+  /** command perspective **/
+
+  def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
+  {
+    if (perspective.isEmpty) Nil
+    else {
+      val result = new mutable.ListBuffer[Command]
+      @tailrec
+      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
+      {
+        (ranges, commands) match {
+          case (range :: more_ranges, (command, offset) #:: more_commands) =>
+            val command_range = command.range + offset
+            range compare command_range match {
+              case -1 => check_ranges(more_ranges, commands)
+              case 0 =>
+                result += command
+                check_ranges(ranges, more_commands)
+              case 1 => check_ranges(ranges, more_commands)
+            }
+          case _ =>
+        }
+      }
+      val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
+      check_ranges(perspective, node.command_range(perspective_range).toStream)
+      result.toList
+    }
+  }
+
+
+
   /** text edits **/
 
   def text_edits(
@@ -138,7 +169,7 @@
 
     @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     {
-      commands.iterator.find(_.is_unparsed) match {
+      commands.iterator.find(cmd => !cmd.is_defined) match {
         case Some(first_unparsed) =>
           val first =
             commands.reverse_iterator(first_unparsed).
@@ -210,6 +241,14 @@
             doc_edits += (name -> Document.Node.Header(header))
             nodes += (name -> node.copy(header = header))
           }
+
+        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))
+          }
       }
       (doc_edits.toList, Document.Version(Document.new_id(), nodes))
     }
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -60,10 +60,29 @@
 class Document_Model(val session: Session, val buffer: Buffer,
   val master_dir: String, val node_name: String, val thy_name: String)
 {
-  /* pending text edits */
+  /* header */
 
   def node_header(): Exn.Result[Thy_Header] =
+  {
+    Swing_Thread.require()
     Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
+  }
+
+
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        doc_view <- Isabelle.document_views(buffer)
+        range <- doc_view.perspective()
+      } yield range)
+  }
+
+
+  /* pending text edits */
 
   private object pending_edits  // owned by Swing thread
   {
@@ -77,14 +96,15 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(node_name, master_dir, node_header(), edits)
+          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
+      session.init_node(node_name, master_dir,
+        node_header(), perspective(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -10,6 +10,7 @@
 
 import isabelle._
 
+import scala.collection.mutable
 import scala.actors.Actor._
 
 import java.lang.System
@@ -86,7 +87,7 @@
   }
 
 
-  /* visible line ranges */
+  /* visible text range */
 
   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
   // NB: jEdit already normalizes \r\n and \r to \n
@@ -96,14 +97,14 @@
     Text.Range(start, stop)
   }
 
-  def screen_lines_range(): Text.Range =
+  def visible_range(): Text.Range =
   {
     val start = text_area.getScreenLineStartOffset(0)
     val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
     proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
   }
 
-  def invalidate_line_range(range: Text.Range)
+  def invalidate_range(range: Text.Range)
   {
     text_area.invalidateLineRange(
       model.buffer.getLineOfOffset(range.start),
@@ -111,6 +112,22 @@
   }
 
 
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        i <- 0 until text_area.getVisibleLines
+        val start = text_area.getScreenLineStartOffset(i)
+        val stop = text_area.getScreenLineEndOffset(i)
+        if start >= 0 && stop >= 0
+      }
+      yield Text.Range(start, stop))
+  }
+
+
   /* snapshot */
 
   // owned by Swing thread
@@ -224,9 +241,9 @@
 
           if (control) init_popup(snapshot, x, y)
 
-          _highlight_range map { case (range, _) => invalidate_line_range(range) }
+          _highlight_range map { case (range, _) => invalidate_range(range) }
           _highlight_range = if (control) subexp_range(snapshot, x, y) else None
-          _highlight_range map { case (range, _) => invalidate_line_range(range) }
+          _highlight_range map { case (range, _) => invalidate_range(range) }
         }
     }
   }
@@ -415,15 +432,15 @@
           val buffer = model.buffer
           Isabelle.swing_buffer_lock(buffer) {
             val (updated, snapshot) = flush_snapshot()
-            val visible_range = screen_lines_range()
+            val visible = visible_range()
 
             if (updated || changed.exists(snapshot.node.commands.contains))
               overview.repaint()
 
-            if (updated) invalidate_line_range(visible_range)
+            if (updated) invalidate_range(visible)
             else {
               val visible_cmds =
-                snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+                snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
               if (visible_cmds.exists(changed)) {
                 for {
                   line <- 0 until text_area.getVisibleLines
diff -r 867928fe20e9 -r 8d6869a8d4ec src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 23 16:37:23 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 23 17:12:54 2011 +0200
@@ -199,6 +199,13 @@
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
 
+  def document_views(buffer: Buffer): List[Document_View] =
+    for {
+      text_area <- jedit_text_areas(buffer).toList
+      val doc_view = document_view(text_area)
+      if doc_view.isDefined
+    } yield doc_view.get
+
   def init_model(buffer: Buffer)
   {
     swing_buffer_lock(buffer) {