# HG changeset patch # User wenzelm # Date 1314042122 -7200 # Node ID 8f6054a63f965459d452fe7e6a95e2c5ca0e5a37 # Parent f99906c2a1d3afd824f0e18c03000721269e40a8 some support for editor perspective; diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/command.scala --- 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 } diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/document.ML --- 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); diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/document.scala --- 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()) diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/isar_document.ML --- 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; diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/isar_document.scala --- 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) diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/PIDE/text.scala --- 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 = { diff -r f99906c2a1d3 -r 8f6054a63f96 src/Pure/System/session.scala --- 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) }