apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
authorwenzelm
Fri Aug 10 15:14:45 2012 +0200 (2012-08-10 ago)
changeset 48755393a37003851
parent 48754 c2c1e5944536
child 48756 1c843142758e
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
expand Clear edit before sending to prover;
at most one full reparse of each node;
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 10 13:33:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 10 15:14:45 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val print_id: id -> string
     1.5    type node_header = string * Thy_Header.header * string list
     1.6    datatype node_edit =
     1.7 -    Clear |
     1.8 +    Clear |    (* FIXME unused !? *)
     1.9      Edits of (command_id option * command_id option) list |
    1.10      Deps of node_header |
    1.11      Perspective of command_id list
     2.1 --- a/src/Pure/PIDE/protocol.ML	Fri Aug 10 13:33:07 2012 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Aug 10 15:14:45 2012 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4              let open XML.Decode in
     2.5                list (pair string
     2.6                  (variant
     2.7 -                 [fn ([], []) => Document.Clear,
     2.8 +                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
     2.9                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    2.10                    fn ([], a) =>
    2.11                      let
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Aug 10 13:33:07 2012 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Aug 10 15:14:45 2012 +0200
     3.3 @@ -213,7 +213,7 @@
     3.4        def encode_edit(name: Document.Node.Name)
     3.5            : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
     3.6          variant(List(
     3.7 -          { case Document.Node.Clear() => (Nil, Nil) },
     3.8 +          { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
     3.9            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    3.10            { case Document.Node.Deps(header) =>
    3.11                val dir = Isabelle_System.posix_path(name.dir)
     4.1 --- a/src/Pure/System/session.scala	Fri Aug 10 13:33:07 2012 +0200
     4.2 +++ b/src/Pure/System/session.scala	Fri Aug 10 15:14:45 2012 +0200
     4.3 @@ -453,7 +453,7 @@
     4.4      header: Document.Node.Header, perspective: Text.Perspective, text: String)
     4.5    {
     4.6      edit(List(header_edit(name, header),
     4.7 -      name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
     4.8 +      name -> Document.Node.Clear(),
     4.9        name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
    4.10        name -> Document.Node.Perspective(perspective)))
    4.11    }
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 10 13:33:07 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 10 15:14:45 2012 +0200
     5.3 @@ -165,7 +165,7 @@
     5.4  
     5.5    /** text edits **/
     5.6  
     5.7 -  /* phase 1: edit individual command source */
     5.8 +  /* edit individual command source */
     5.9  
    5.10    @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
    5.11        : Linear_Set[Command] =
    5.12 @@ -194,7 +194,7 @@
    5.13    }
    5.14  
    5.15  
    5.16 -  /* phase 2a: reparse range of command spans */
    5.17 +  /* reparse range of command spans */
    5.18  
    5.19    @tailrec private def chop_common(
    5.20        cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
    5.21 @@ -230,8 +230,9 @@
    5.22    }
    5.23  
    5.24  
    5.25 -  /* phase 2b: recover command spans after edits */
    5.26 +  /* recover command spans after edits */
    5.27  
    5.28 +  // FIXME somewhat slow
    5.29    private def recover_spans(
    5.30      syntax: Outer_Syntax,
    5.31      name: Document.Node.Name,
    5.32 @@ -256,7 +257,7 @@
    5.33    }
    5.34  
    5.35  
    5.36 -  /* phase 2c: consolidate unfinished spans */
    5.37 +  /* consolidate unfinished spans */
    5.38  
    5.39    private def consolidate_spans(
    5.40      syntax: Outer_Syntax,
    5.41 @@ -280,7 +281,7 @@
    5.42    }
    5.43  
    5.44  
    5.45 -  /* main phase */
    5.46 +  /* main */
    5.47  
    5.48    private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
    5.49      : List[(Option[Command], Option[Command])] =
    5.50 @@ -292,6 +293,29 @@
    5.51      inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
    5.52    }
    5.53  
    5.54 +  private def text_edit(syntax: Outer_Syntax,
    5.55 +    node: Document.Node, edit: Document.Edit_Text): Document.Node =
    5.56 +  {
    5.57 +    edit match {
    5.58 +      case (_, Document.Node.Clear()) => node.clear
    5.59 +
    5.60 +      case (name, Document.Node.Edits(text_edits)) =>
    5.61 +        val commands0 = node.commands
    5.62 +        val commands1 = edit_text(text_edits, commands0)
    5.63 +        val commands2 = recover_spans(syntax, name, node.perspective, commands1)
    5.64 +        node.update_commands(commands2)
    5.65 +
    5.66 +      case (_, Document.Node.Deps(_)) => node
    5.67 +
    5.68 +      case (name, Document.Node.Perspective(text_perspective)) =>
    5.69 +        val perspective = command_perspective(node, text_perspective)
    5.70 +        if (node.perspective same perspective) node
    5.71 +        else
    5.72 +          node.update_perspective(perspective)
    5.73 +            .update_commands(consolidate_spans(syntax, name, perspective, node.commands))
    5.74 +    }
    5.75 +  }
    5.76 +
    5.77    def text_edits(
    5.78        base_syntax: Outer_Syntax,
    5.79        previous: Document.Version,
    5.80 @@ -304,38 +328,27 @@
    5.81      var nodes = nodes0
    5.82      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
    5.83  
    5.84 -    (edits ::: reparse.map((_, Document.Node.Edits(Nil)))) foreach {
    5.85 -      case (name, Document.Node.Clear()) =>
    5.86 -        doc_edits += (name -> Document.Node.Clear())
    5.87 -        nodes += (name -> nodes(name).clear)
    5.88 -
    5.89 -      case (name, Document.Node.Edits(text_edits)) =>
    5.90 -        val node = nodes(name)
    5.91 +    val node_edits =
    5.92 +      (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
    5.93 +        .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
    5.94  
    5.95 -        val commands0 = node.commands
    5.96 -        val commands1 = edit_text(text_edits, commands0)
    5.97 -        val commands2 = recover_spans(syntax, name, node.perspective, commands1)   // FIXME somewhat slow
    5.98 -        val commands3 =
    5.99 -          if (reparse_set.contains(name) && !commands2.isEmpty)
   5.100 -            reparse_spans(syntax, name, commands2, commands2.head, commands2.last)  // FIXME somewhat slow
   5.101 -          else commands2
   5.102 +    node_edits foreach {
   5.103 +      case (name, edits) =>
   5.104 +        val node = nodes(name)
   5.105 +        val commands = node.commands
   5.106  
   5.107 -        doc_edits += (name -> Document.Node.Edits(diff_commands(commands0, commands3)))
   5.108 -        nodes += (name -> node.update_commands(commands3))
   5.109 -
   5.110 -      case (name, Document.Node.Deps(_)) =>
   5.111 +        val node1 =
   5.112 +          if (reparse_set(name) && !commands.isEmpty)
   5.113 +            node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
   5.114 +          else node
   5.115 +        val node2 = (node1 /: edits)(text_edit(syntax, _, _))
   5.116  
   5.117 -      case (name, Document.Node.Perspective(text_perspective)) =>
   5.118 -        val node = nodes(name)
   5.119 -        val perspective = command_perspective(node, text_perspective)
   5.120 -        if (!(node.perspective same perspective)) {
   5.121 -/* FIXME
   5.122 -          val commands1 = consolidate_spans(syntax, name, perspective, node.commands)
   5.123 -          doc_edits += (name -> Document.Node.Edits(diff_commands(node.commands, commands1)))
   5.124 -*/
   5.125 -          doc_edits += (name -> Document.Node.Perspective(perspective))
   5.126 -          nodes += (name -> node.update_perspective(perspective))
   5.127 -        }
   5.128 +        if (!(node.perspective same node2.perspective))
   5.129 +          doc_edits += (name -> Document.Node.Perspective(node2.perspective))
   5.130 +
   5.131 +        doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   5.132 +
   5.133 +        nodes += (name -> node2)
   5.134      }
   5.135  
   5.136      (doc_edits.toList, Document.Version.make(syntax, nodes))