1.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 22 21:42:02 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 23 12:20:12 2011 +0200
     1.3 @@ -89,6 +89,14 @@
     1.4    /* perspective */
     1.5  
     1.6    type Perspective = List[Command]  // visible commands in canonical order
     1.7 +
     1.8 +  def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
     1.9 +  {
    1.10 +    require(p1.forall(_.is_defined))
    1.11 +    require(p2.forall(_.is_defined))
    1.12 +    p1.length == p2.length &&
    1.13 +      (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
    1.14 +  }
    1.15  }
    1.16  
    1.17  
    1.18 @@ -98,12 +106,12 @@
    1.19  {
    1.20    /* classification */
    1.21  
    1.22 +  def is_defined: Boolean = id != Document.no_id
    1.23 +
    1.24    def is_command: Boolean = !span.isEmpty && span.head.is_command
    1.25    def is_ignored: Boolean = span.forall(_.is_ignored)
    1.26    def is_malformed: Boolean = !is_command && !is_ignored
    1.27  
    1.28 -  def is_unparsed = id == Document.no_id
    1.29 -
    1.30    def name: String = if (is_command) span.head.content else ""
    1.31    override def toString =
    1.32      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")

     2.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 22 21:42:02 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 23 12:20:12 2011 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4      Clear |
     2.5      Edits of (command_id option * command_id option) list |
     2.6      Header of node_header |
     2.7 -    Perspective of id list
     2.8 +    Perspective of command_id list
     2.9    type edit = string * node_edit
    2.10    type state
    2.11    val init_state: state
    2.12 @@ -61,30 +61,38 @@
    2.13  
    2.14  abstype node = Node of
    2.15   {header: node_header,
    2.16 +  perspective: command_id list,
    2.17    entries: exec_id option Entries.T,  (*command entries with excecutions*)
    2.18    result: Toplevel.state lazy}
    2.19  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    2.20  with
    2.21  
    2.22 -fun make_node (header, entries, result) =
    2.23 -  Node {header = header, entries = entries, result = result};
    2.24 +fun make_node (header, perspective, entries, result) =
    2.25 +  Node {header = header, perspective = perspective, entries = entries, result = result};
    2.26  
    2.27 -fun map_node f (Node {header, entries, result}) =
    2.28 -  make_node (f (header, entries, result));
    2.29 +fun map_node f (Node {header, perspective, entries, result}) =
    2.30 +  make_node (f (header, perspective, entries, result));
    2.31  
    2.32  fun get_header (Node {header, ...}) = header;
    2.33 -fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
    2.34 +fun set_header header =
    2.35 +  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    2.36  
    2.37 -fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
    2.38 +fun get_perspective (Node {perspective, ...}) = perspective;
    2.39 +fun set_perspective perspective =
    2.40 +  map_node (fn (header, _, entries, result) => (header, perspective, entries, result));
    2.41 +
    2.42 +fun map_entries f (Node {header, perspective, entries, result}) =
    2.43 +  make_node (header, perspective, f entries, result);
    2.44  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    2.45  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    2.46  
    2.47  fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
    2.48 -fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
    2.49 +fun set_result result =
    2.50 +  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
    2.51  
    2.52  val empty_exec = Lazy.value Toplevel.toplevel;
    2.53 -val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
    2.54 -val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
    2.55 +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), [], Entries.empty, empty_exec);
    2.56 +val clear_node = map_node (fn (header, _, _, _) => (header, [], Entries.empty, empty_exec));
    2.57  
    2.58  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    2.59  fun default_node name = Graph.default_node (name, empty_node);
    2.60 @@ -97,7 +105,7 @@
    2.61    Clear |
    2.62    Edits of (command_id option * command_id option) list |
    2.63    Header of node_header |
    2.64 -  Perspective of id list;
    2.65 +  Perspective of command_id list;
    2.66  
    2.67  type edit = string * node_edit;
    2.68  
    2.69 @@ -153,7 +161,8 @@
    2.70                (header, Graph.add_deps_acyclic (name, parents) nodes2)
    2.71                  handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    2.72            in Graph.map_node name (set_header header') nodes3 end
    2.73 -      | Perspective _ => nodes));  (* FIXME *)
    2.74 +      | Perspective perspective =>
    2.75 +          update_node name (set_perspective perspective) nodes));
    2.76  
    2.77  fun put_node (name, node) (Version nodes) =
    2.78    Version (update_node name (K node) nodes);
    2.79 @@ -354,9 +363,10 @@
    2.80                          | NONE =>
    2.81                              get_theory (Position.file_only import)
    2.82                                (#2 (Future.join (the (AList.lookup (op =) deps import))))));
    2.83 -                  in Thy_Load.begin_theory dir thy_name imports files parents end
    2.84 +                  in Thy_Load.begin_theory dir thy_name imports files parents end;
    2.85                  fun get_command id =
    2.86                    (id, the_command state id |> Future.map (Toplevel.modify_init init));
    2.87 +                val perspective = get_perspective node;  (* FIXME *)
    2.88                in
    2.89                  (singleton o Future.forks)
    2.90                    {name = "Document.edit", group = NONE,

     3.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 22 21:42:02 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 23 12:20:12 2011 +0200
     3.3 @@ -61,7 +61,7 @@
     3.4          case exn => Header[A, B](exn)
     3.5        }
     3.6  
     3.7 -    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
     3.8 +    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
     3.9  
    3.10      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    3.11        : Iterator[(Command, Text.Offset)] =
    3.12 @@ -79,6 +79,7 @@
    3.13  
    3.14    sealed case class Node(
    3.15      val header: Node_Header,
    3.16 +    val perspective: Command.Perspective,
    3.17      val blobs: Map[String, Blob],
    3.18      val commands: Linear_Set[Command])
    3.19    {

     4.1 --- a/src/Pure/System/session.scala	Mon Aug 22 21:42:02 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Tue Aug 23 12:20:12 2011 +0200
     4.3 @@ -164,10 +164,10 @@
     4.4  
     4.5    private case class Start(timeout: Time, args: List[String])
     4.6    private case object Interrupt
     4.7 -  private case class Init_Node(
     4.8 -    name: String, master_dir: String, header: Document.Node_Header, text: String)
     4.9 -  private case class Edit_Node(
    4.10 -    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
    4.11 +  private case class Init_Node(name: String, master_dir: String,
    4.12 +    header: Document.Node_Header, perspective: Text.Perspective, text: String)
    4.13 +  private case class Edit_Node(name: String, master_dir: String,
    4.14 +    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
    4.15    private case class Change_Node(
    4.16      name: String,
    4.17      doc_edits: List[Document.Edit_Command],
    4.18 @@ -336,14 +336,18 @@
    4.19          case Interrupt if prover.isDefined =>
    4.20            prover.get.interrupt
    4.21  
    4.22 -        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
    4.23 +        case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
    4.24            // FIXME compare with existing node
    4.25            handle_edits(name, master_dir, header,
    4.26 -            List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
    4.27 +            List(Document.Node.Clear(),
    4.28 +              Document.Node.Edits(List(Text.Edit.insert(0, text))),
    4.29 +              Document.Node.Perspective(perspective)))
    4.30            reply(())
    4.31  
    4.32 -        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
    4.33 -          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
    4.34 +        case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
    4.35 +          handle_edits(name, master_dir, header,
    4.36 +            List(Document.Node.Edits(text_edits),
    4.37 +              Document.Node.Perspective(perspective)))
    4.38            reply(())
    4.39  
    4.40          case change: Change_Node if prover.isDefined =>
    4.41 @@ -371,9 +375,13 @@
    4.42  
    4.43    def interrupt() { session_actor ! Interrupt }
    4.44  
    4.45 -  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
    4.46 -  { session_actor !? Init_Node(name, master_dir, header, text) }
    4.47 +  // FIXME simplify signature
    4.48 +  def init_node(name: String, master_dir: String,
    4.49 +    header: Document.Node_Header, perspective: Text.Perspective, text: String)
    4.50 +  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
    4.51  
    4.52 -  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
    4.53 -  { session_actor !? Edit_Node(name, master_dir, header, edits) }
    4.54 +  // FIXME simplify signature
    4.55 +  def edit_node(name: String, master_dir: String, header: Document.Node_Header,
    4.56 +    perspective: Text.Perspective, edits: List[Text.Edit])
    4.57 +  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
    4.58  }

     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 22 21:42:02 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 12:20:12 2011 +0200
     5.3 @@ -138,7 +138,7 @@
     5.4  
     5.5      @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     5.6      {
     5.7 -      commands.iterator.find(_.is_unparsed) match {
     5.8 +      commands.iterator.find(cmd => !cmd.is_defined) match {
     5.9          case Some(first_unparsed) =>
    5.10            val first =
    5.11              commands.reverse_iterator(first_unparsed).
    5.12 @@ -172,6 +172,37 @@
    5.13      }
    5.14  
    5.15  
    5.16 +    /* command perspective */
    5.17 +
    5.18 +    def command_perspective(node: Document.Node, perspective: Text.Perspective)
    5.19 +        : Command.Perspective =
    5.20 +    {
    5.21 +      if (perspective.isEmpty) Nil
    5.22 +      else {
    5.23 +        val result = new mutable.ListBuffer[Command]
    5.24 +        @tailrec
    5.25 +        def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
    5.26 +        {
    5.27 +          (ranges, commands) match {
    5.28 +            case (range :: more_ranges, (command, offset) #:: more_commands) =>
    5.29 +              val command_range = command.range + offset
    5.30 +              range compare command_range match {
    5.31 +                case -1 => check_ranges(more_ranges, commands)
    5.32 +                case 0 =>
    5.33 +                  result += command
    5.34 +                  check_ranges(ranges, more_commands)
    5.35 +                case 1 => check_ranges(ranges, more_commands)
    5.36 +              }
    5.37 +            case _ =>
    5.38 +          }
    5.39 +        }
    5.40 +        val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
    5.41 +        check_ranges(perspective, node.command_range(perspective_range).toStream)
    5.42 +        result.toList
    5.43 +      }
    5.44 +    }
    5.45 +
    5.46 +
    5.47      /* resulting document edits */
    5.48  
    5.49      {
    5.50 @@ -210,6 +241,14 @@
    5.51              doc_edits += (name -> Document.Node.Header(header))
    5.52              nodes += (name -> node.copy(header = header))
    5.53            }
    5.54 +
    5.55 +        case (name, Document.Node.Perspective(text_perspective)) =>
    5.56 +          val node = nodes(name)
    5.57 +          val perspective = command_perspective(node, text_perspective)
    5.58 +          if (!Command.equal_perspective(node.perspective, perspective)) {
    5.59 +            doc_edits += (name -> Document.Node.Perspective(perspective))
    5.60 +            nodes += (name -> node.copy(perspective = perspective))
    5.61 +          }
    5.62        }
    5.63        (doc_edits.toList, Document.Version(Document.new_id(), nodes))
    5.64      }

     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 21:42:02 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 12:20:12 2011 +0200
     6.3 @@ -60,10 +60,29 @@
     6.4  class Document_Model(val session: Session, val buffer: Buffer,
     6.5    val master_dir: String, val node_name: String, val thy_name: String)
     6.6  {
     6.7 -  /* pending text edits */
     6.8 +  /* header */
     6.9  
    6.10    def node_header(): Exn.Result[Thy_Header] =
    6.11 +  {
    6.12 +    Swing_Thread.require()
    6.13      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
    6.14 +  }
    6.15 +
    6.16 +
    6.17 +  /* perspective */
    6.18 +
    6.19 +  def perspective(): Text.Perspective =
    6.20 +  {
    6.21 +    Swing_Thread.require()
    6.22 +    Text.perspective(
    6.23 +      for {
    6.24 +        doc_view <- Isabelle.document_views(buffer)
    6.25 +        range <- doc_view.perspective()
    6.26 +      } yield range)
    6.27 +  }
    6.28 +
    6.29 +
    6.30 +  /* pending text edits */
    6.31  
    6.32    private object pending_edits  // owned by Swing thread
    6.33    {
    6.34 @@ -77,14 +96,15 @@
    6.35          case Nil =>
    6.36          case edits =>
    6.37            pending.clear
    6.38 -          session.edit_node(node_name, master_dir, node_header(), edits)
    6.39 +          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
    6.40        }
    6.41      }
    6.42  
    6.43      def init()
    6.44      {
    6.45        flush()
    6.46 -      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
    6.47 +      session.init_node(node_name, master_dir,
    6.48 +        node_header(), perspective(), Isabelle.buffer_text(buffer))
    6.49      }
    6.50  
    6.51      private val delay_flush =
    6.52 @@ -99,19 +119,6 @@
    6.53    }
    6.54  
    6.55  
    6.56 -  /* perspective */
    6.57 -
    6.58 -  def perspective(): Text.Perspective =
    6.59 -  {
    6.60 -    Swing_Thread.require()
    6.61 -    Text.perspective(
    6.62 -      for {
    6.63 -        doc_view <- Isabelle.document_views(buffer)
    6.64 -        range <- doc_view.perspective()
    6.65 -      } yield range)
    6.66 -  }
    6.67 -
    6.68 -
    6.69    /* snapshot */
    6.70  
    6.71    def snapshot(): Document.Snapshot =