# HG changeset patch
# User wenzelm
# Date 1314094812 -7200
# Node ID e7fdb008aa7d2631c63e6ecb44e1f78b27bdd8ba
# Parent  8f6054a63f965459d452fe7e6a95e2c5ca0e5a37
propagate editor perspective through document model;

diff -r 8f6054a63f96 -r e7fdb008aa7d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 23 12:20:12 2011 +0200
@@ -89,6 +89,14 @@
   /* 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 })
+  }
 }
 
 
@@ -98,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 8f6054a63f96 -r e7fdb008aa7d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 23 12:20:12 2011 +0200
@@ -20,7 +20,7 @@
     Clear |
     Edits of (command_id option * command_id option) list |
     Header of node_header |
-    Perspective of id list
+    Perspective of command_id list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -61,30 +61,38 @@
 
 abstype node = Node of
  {header: node_header,
+  perspective: command_id list,
   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, entries, result}) =
-  make_node (f (header, entries, result));
+fun map_node f (Node {header, perspective, entries, result}) =
+  make_node (f (header, perspective, entries, result));
 
 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 =
+  map_node (fn (header, _, entries, result) => (header, perspective, entries, result));
+
+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));
+fun set_result result =
+  map_node (fn (header, perspective, entries, _) => (header, perspective, 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));
+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_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
 fun default_node name = Graph.default_node (name, empty_node);
@@ -97,7 +105,7 @@
   Clear |
   Edits of (command_id option * command_id option) list |
   Header of node_header |
-  Perspective of id list;
+  Perspective of command_id list;
 
 type edit = string * node_edit;
 
@@ -153,7 +161,8 @@
               (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 _ => nodes));  (* FIXME *)
+      | Perspective perspective =>
+          update_node name (set_perspective perspective) nodes));
 
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);
@@ -354,9 +363,10 @@
                         | 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));
+                val perspective = get_perspective node;  (* FIXME *)
               in
                 (singleton o Future.forks)
                   {name = "Document.edit", group = NONE,
diff -r 8f6054a63f96 -r e7fdb008aa7d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 23 12:20:12 2011 +0200
@@ -61,7 +61,7 @@
         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)] =
@@ -79,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 8f6054a63f96 -r e7fdb008aa7d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 23 12:20:12 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],
@@ -336,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 =>
@@ -371,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 8f6054a63f96 -r e7fdb008aa7d src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 12:20:12 2011 +0200
@@ -138,7 +138,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).
@@ -172,6 +172,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
+      }
+    }
+
+
     /* resulting document edits */
 
     {
@@ -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 8f6054a63f96 -r e7fdb008aa7d src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 21:42:02 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 12:20:12 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 =
@@ -99,19 +119,6 @@
   }
 
 
-  /* perspective */
-
-  def perspective(): Text.Perspective =
-  {
-    Swing_Thread.require()
-    Text.perspective(
-      for {
-        doc_view <- Isabelle.document_views(buffer)
-        range <- doc_view.perspective()
-      } yield range)
-  }
-
-
   /* snapshot */
 
   def snapshot(): Document.Snapshot =