clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
authorwenzelm
Fri Nov 22 21:13:44 2013 +0100 (2013-11-22)
changeset 54562301a721af68b
parent 54561 ceb190f4f69f
child 54563 7fa522b213a8
child 54568 08b642269a0d
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Nov 22 20:54:26 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Nov 22 21:13:44 2013 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4    type node_header = string * Thy_Header.header * string list
     1.5    type overlay = Document_ID.command * (string * string list)
     1.6    datatype node_edit =
     1.7 -    Clear |    (* FIXME unused !? *)
     1.8      Edits of (Document_ID.command option * Document_ID.command option) list |
     1.9      Deps of node_header |
    1.10      Perspective of bool * Document_ID.command list * overlay list
    1.11 @@ -76,7 +75,6 @@
    1.12  val no_perspective = make_perspective (false, [], []);
    1.13  
    1.14  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.15 -val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
    1.16  
    1.17  
    1.18  (* basic components *)
    1.19 @@ -145,7 +143,6 @@
    1.20  type overlay = Document_ID.command * (string * string list);
    1.21  
    1.22  datatype node_edit =
    1.23 -  Clear |
    1.24    Edits of (Document_ID.command option * Document_ID.command option) list |
    1.25    Deps of node_header |
    1.26    Perspective of bool * Document_ID.command list * overlay list;
    1.27 @@ -193,8 +190,7 @@
    1.28  fun edit_nodes (name, node_edit) (Version nodes) =
    1.29    Version
    1.30      (case node_edit of
    1.31 -      Clear => update_node name clear_node nodes
    1.32 -    | Edits edits => update_node name (edit_node edits) nodes
    1.33 +      Edits edits => update_node name (edit_node edits) nodes
    1.34      | Deps (master, header, errors) =>
    1.35          let
    1.36            val imports = map fst (#imports header);
     2.1 --- a/src/Pure/PIDE/document.scala	Fri Nov 22 20:54:26 2013 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Nov 22 21:13:44 2013 +0100
     2.3 @@ -127,10 +127,11 @@
     2.4        }
     2.5      }
     2.6      case class Clear[A, B]() extends Edit[A, B]
     2.7 +    case class Blob[A, B]() extends Edit[A, B]
     2.8 +
     2.9      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    2.10      case class Deps[A, B](header: Header) extends Edit[A, B]
    2.11      case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
    2.12 -    case class Blob[A, B]() extends Edit[A, B]
    2.13      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    2.14      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    2.15  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Fri Nov 22 20:54:26 2013 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Nov 22 21:13:44 2013 +0100
     3.3 @@ -62,8 +62,7 @@
     3.4              let open XML.Decode in
     3.5                list (pair string
     3.6                  (variant
     3.7 -                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
     3.8 -                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     3.9 +                 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    3.10                    fn ([], a) =>
    3.11                      let
    3.12                        val (master, (name, (imports, (keywords, errors)))) =
     4.1 --- a/src/Pure/PIDE/protocol.scala	Fri Nov 22 20:54:26 2013 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Nov 22 21:13:44 2013 +0100
     4.3 @@ -352,8 +352,6 @@
     4.4        def encode_edit(name: Document.Node.Name)
     4.5            : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
     4.6          variant(List(
     4.7 -          // FIXME Document.Node.Blob (!??)
     4.8 -          { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
     4.9            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    4.10            { case Document.Node.Deps(header) =>
    4.11                val master_dir = Isabelle_System.posix_path(name.master_dir)
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Nov 22 20:54:26 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Nov 22 21:13:44 2013 +0100
     5.3 @@ -397,6 +397,8 @@
     5.4      edit match {
     5.5        case (_, Document.Node.Clear()) => node.clear
     5.6  
     5.7 +      case (_, Document.Node.Blob()) => node
     5.8 +
     5.9        case (name, Document.Node.Edits(text_edits)) =>
    5.10          val commands0 = node.commands
    5.11          val commands1 = edit_text(text_edits, commands0)
    5.12 @@ -415,8 +417,6 @@
    5.13            node.update_perspective(perspective).update_commands(
    5.14              consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
    5.15                name, visible, node.commands))
    5.16 -
    5.17 -      case (_, Document.Node.Blob()) => node
    5.18      }
    5.19    }
    5.20