some support for editor perspective;

--- a/src/Pure/PIDE/command.scala	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 22 21:42:02 2011 +0200
@@ -84,6 +84,11 @@
 
   def span(toks: List[Token]): Command =
     new Command(Document.no_id, toks)
+
+
+  /* perspective */
+
+  type Perspective = List[Command]  // visible commands in canonical order
 }
 
 

--- a/src/Pure/PIDE/document.ML	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 22 21:42:02 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 id list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -95,7 +96,8 @@
 datatype node_edit =
   Clear |
   Edits of (command_id option * command_id option) list |
-  Header of node_header;
+  Header of node_header |
+  Perspective of id list;
 
 type edit = string * node_edit;
 
@@ -150,7 +152,8 @@
             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 _ => nodes));  (* FIXME *)
 
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);

--- a/src/Pure/PIDE/document.scala	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 22 21:42:02 2011 +0200
@@ -31,15 +31,15 @@
 
   /* 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[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 foreach(f: A => Unit)
       {
@@ -49,14 +49,16 @@
         }
       }
     }
-    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())

--- a/src/Pure/PIDE/isar_document.ML	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Mon Aug 22 21:42:02 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;

--- a/src/Pure/PIDE/isar_document.scala	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Mon Aug 22 21:42:02 2011 +0200
@@ -152,7 +152,8 @@
             { 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)

--- a/src/Pure/PIDE/text.scala	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Aug 22 21:42:02 2011 +0200
@@ -62,7 +62,7 @@
 
   /* perspective */
 
-  type Perspective = List[Range]  // partitioning in canonical order
+  type Perspective = List[Range]  // visible text partitioning in canonical order
 
   def perspective(ranges: Seq[Range]): Perspective =
   {

--- a/src/Pure/System/session.scala	Mon Aug 22 21:09:26 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 22 21:42:02 2011 +0200
@@ -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) }