more scalable on 32-bit Poly/ML;
authorwenzelm
Thu Feb 28 21:37:24 2019 +0100 (7 weeks ago ago)
changeset 7003009f200c658ed
parent 70029 bf2cd27714fb
child 70031 5f993636ac07
more scalable on 32-bit Poly/ML;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.ML	Thu Feb 28 21:16:17 2019 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Feb 28 21:37:24 2019 +0100
     1.3 @@ -74,15 +74,18 @@
     1.4  val _ =
     1.5    Isabelle_Process.protocol_command "Document.update"
     1.6      (Future.task_context "Document.update" (Future.new_group NONE)
     1.7 -      (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
     1.8 +      (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
     1.9          Document.change_state (fn state =>
    1.10            let
    1.11              val old_id = Document_ID.parse old_id_string;
    1.12              val new_id = Document_ID.parse new_id_string;
    1.13 +            val consolidate =
    1.14 +              YXML.parse_body consolidate_yxml |>
    1.15 +                let open XML.Decode in list string end;
    1.16              val edits =
    1.17 -              YXML.parse_body edits_yxml |>
    1.18 +              edits_yxml |> map (YXML.parse_body #>
    1.19                  let open XML.Decode in
    1.20 -                  list (pair string
    1.21 +                  pair string
    1.22                      (variant
    1.23                       [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    1.24                        fn ([], a) =>
    1.25 @@ -98,11 +101,8 @@
    1.26                          in Document.Deps {master = master, header = header, errors = errors} end,
    1.27                        fn (a :: b, c) =>
    1.28                          Document.Perspective (bool_atom a, map int_atom b,
    1.29 -                          list (pair int (pair string (list string))) c)]))
    1.30 -                end;
    1.31 -            val consolidate =
    1.32 -              YXML.parse_body consolidate_yxml |>
    1.33 -                let open XML.Decode in list string end;
    1.34 +                          list (pair int (pair string (list string))) c)])
    1.35 +                end);
    1.36  
    1.37              val _ = Execution.discontinue ();
    1.38  
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Feb 28 21:16:17 2019 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Feb 28 21:37:24 2019 +0100
     2.3 @@ -283,6 +283,11 @@
     2.4    def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     2.5      edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
     2.6    {
     2.7 +    val consolidate_yxml =
     2.8 +    {
     2.9 +      import XML.Encode._
    2.10 +      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
    2.11 +    }
    2.12      val edits_yxml =
    2.13      {
    2.14        import XML.Encode._
    2.15 @@ -303,22 +308,11 @@
    2.16            { case Document.Node.Perspective(a, b, c) =>
    2.17                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    2.18                  list(pair(id, pair(string, list(string))))(c.dest)) }))
    2.19 -      def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    2.20 -      {
    2.21 -        val (name, edit) = node_edit
    2.22 -        pair(string, encode_edit(name))(name.node, edit)
    2.23 -      })
    2.24 -      Symbol.encode_yxml(encode_edits(edits))
    2.25 +      edits.map({ case (name, edit) =>
    2.26 +        Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
    2.27      }
    2.28 -
    2.29 -    val consolidate_yxml =
    2.30 -    {
    2.31 -      import XML.Encode._
    2.32 -      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
    2.33 -    }
    2.34 -
    2.35 -    protocol_command(
    2.36 -      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate_yxml)
    2.37 +    protocol_command("Document.update",
    2.38 +      (Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml): _*)
    2.39    }
    2.40  
    2.41    def remove_versions(versions: List[Document.Version])