some support for editor perspective;
authorwenzelm
Mon Aug 22 21:42:02 2011 +0200 (2011-08-22)
changeset 443848f6054a63f96
parent 44383 f99906c2a1d3
child 44385 e7fdb008aa7d
some support for editor perspective;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/PIDE/text.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 22 21:09:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Aug 22 21:42:02 2011 +0200
     1.3 @@ -84,6 +84,11 @@
     1.4  
     1.5    def span(toks: List[Token]): Command =
     1.6      new Command(Document.no_id, toks)
     1.7 +
     1.8 +
     1.9 +  /* perspective */
    1.10 +
    1.11 +  type Perspective = List[Command]  // visible commands in canonical order
    1.12  }
    1.13  
    1.14  
     2.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 22 21:09:26 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 22 21:42:02 2011 +0200
     2.3 @@ -19,7 +19,8 @@
     2.4    datatype node_edit =
     2.5      Clear |
     2.6      Edits of (command_id option * command_id option) list |
     2.7 -    Header of node_header
     2.8 +    Header of node_header |
     2.9 +    Perspective of id list
    2.10    type edit = string * node_edit
    2.11    type state
    2.12    val init_state: state
    2.13 @@ -95,7 +96,8 @@
    2.14  datatype node_edit =
    2.15    Clear |
    2.16    Edits of (command_id option * command_id option) list |
    2.17 -  Header of node_header;
    2.18 +  Header of node_header |
    2.19 +  Perspective of id list;
    2.20  
    2.21  type edit = string * node_edit;
    2.22  
    2.23 @@ -150,7 +152,8 @@
    2.24              val (header', nodes3) =
    2.25                (header, Graph.add_deps_acyclic (name, parents) nodes2)
    2.26                  handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    2.27 -          in Graph.map_node name (set_header header') nodes3 end));
    2.28 +          in Graph.map_node name (set_header header') nodes3 end
    2.29 +      | Perspective _ => nodes));  (* FIXME *)
    2.30  
    2.31  fun put_node (name, node) (Version nodes) =
    2.32    Version (update_node name (K node) nodes);
     3.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 22 21:09:26 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Mon Aug 22 21:42:02 2011 +0200
     3.3 @@ -31,15 +31,15 @@
     3.4  
     3.5    /* named nodes -- development graph */
     3.6  
     3.7 -  type Edit[A] = (String, Node.Edit[A])
     3.8 -  type Edit_Text = Edit[Text.Edit]
     3.9 -  type Edit_Command = Edit[(Option[Command], Option[Command])]
    3.10 +  type Edit[A, B] = (String, Node.Edit[A, B])
    3.11 +  type Edit_Text = Edit[Text.Edit, Text.Perspective]
    3.12 +  type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
    3.13  
    3.14    type Node_Header = Exn.Result[Thy_Header]
    3.15  
    3.16    object Node
    3.17    {
    3.18 -    sealed abstract class Edit[A]
    3.19 +    sealed abstract class Edit[A, B]
    3.20      {
    3.21        def foreach(f: A => Unit)
    3.22        {
    3.23 @@ -49,14 +49,16 @@
    3.24          }
    3.25        }
    3.26      }
    3.27 -    case class Clear[A]() extends Edit[A]
    3.28 -    case class Edits[A](edits: List[A]) extends Edit[A]
    3.29 -    case class Header[A](header: Node_Header) extends Edit[A]
    3.30 +    case class Clear[A, B]() extends Edit[A, B]
    3.31 +    case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    3.32 +    case class Header[A, B](header: Node_Header) extends Edit[A, B]
    3.33 +    case class Perspective[A, B](perspective: B) extends Edit[A, B]
    3.34  
    3.35 -    def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
    3.36 +    def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
    3.37 +        : Header[A, B] =
    3.38        header match {
    3.39 -        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
    3.40 -        case exn => Header[A](exn)
    3.41 +        case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
    3.42 +        case exn => Header[A, B](exn)
    3.43        }
    3.44  
    3.45      val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
     4.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Aug 22 21:09:26 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Aug 22 21:42:02 2011 +0200
     4.3 @@ -27,7 +27,8 @@
     4.4                    fn ([], a) =>
     4.5                      Document.Header
     4.6                        (Exn.Res (triple string (list string) (list (pair string bool)) a)),
     4.7 -                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
     4.8 +                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
     4.9 +                  fn (a, []) => Document.Perspective (map int_atom a)]))
    4.10              end;
    4.11  
    4.12        val running = Document.cancel_execution state;
     5.1 --- a/src/Pure/PIDE/isar_document.scala	Mon Aug 22 21:09:26 2011 +0200
     5.2 +++ b/src/Pure/PIDE/isar_document.scala	Mon Aug 22 21:42:02 2011 +0200
     5.3 @@ -152,7 +152,8 @@
     5.4              { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     5.5              { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
     5.6                  (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
     5.7 -            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
     5.8 +            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
     5.9 +            { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
    5.10        YXML.string_of_body(encode(edits)) }
    5.11  
    5.12      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
     6.1 --- a/src/Pure/PIDE/text.scala	Mon Aug 22 21:09:26 2011 +0200
     6.2 +++ b/src/Pure/PIDE/text.scala	Mon Aug 22 21:42:02 2011 +0200
     6.3 @@ -62,7 +62,7 @@
     6.4  
     6.5    /* perspective */
     6.6  
     6.7 -  type Perspective = List[Range]  // partitioning in canonical order
     6.8 +  type Perspective = List[Range]  // visible text partitioning in canonical order
     6.9  
    6.10    def perspective(ranges: Seq[Range]): Perspective =
    6.11    {
     7.1 --- a/src/Pure/System/session.scala	Mon Aug 22 21:09:26 2011 +0200
     7.2 +++ b/src/Pure/System/session.scala	Mon Aug 22 21:42:02 2011 +0200
     7.3 @@ -183,7 +183,7 @@
     7.4      /* incoming edits */
     7.5  
     7.6      def handle_edits(name: String, master_dir: String,
     7.7 -        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
     7.8 +        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
     7.9      //{{{
    7.10      {
    7.11        val syntax = current_syntax()
    7.12 @@ -196,7 +196,8 @@
    7.13          else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    7.14        }
    7.15        def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
    7.16 -      val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header)
    7.17 +      val norm_header =
    7.18 +        Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header)
    7.19  
    7.20        val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    7.21        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }