clarified YXML vs. symbol encoding: operate on whole message;
authorwenzelm
Sat Apr 01 22:03:24 2017 +0200 (2017-04-01)
changeset 653452fdd4431b30e
parent 65344 b99283eed13c
child 65346 673a7b3379ec
clarified YXML vs. symbol encoding: operate on whole message;
tuned signature;
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/prover.scala
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Apr 01 19:17:15 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 01 22:03:24 2017 +0200
     1.3 @@ -16,8 +16,7 @@
     1.4      def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
     1.5        try {
     1.6          import XML.Decode._
     1.7 -        val body = YXML.parse_body(text)
     1.8 -        Some(pair(long, list(pair(long, list(long))))(body))
     1.9 +        Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
    1.10        }
    1.11        catch {
    1.12          case ERROR(_) => None
    1.13 @@ -30,7 +29,7 @@
    1.14      def unapply(text: String): Option[List[Document_ID.Version]] =
    1.15        try {
    1.16          import XML.Decode._
    1.17 -        Some(list(long)(YXML.parse_body(text)))
    1.18 +        Some(list(long)(Symbol.decode_yxml(text)))
    1.19        }
    1.20        catch {
    1.21          case ERROR(_) => None
    1.22 @@ -291,17 +290,6 @@
    1.23  
    1.24  trait Protocol
    1.25  {
    1.26 -  /* text */
    1.27 -
    1.28 -  def encode(s: String): String
    1.29 -  def decode(s: String): String
    1.30 -
    1.31 -  object Encode
    1.32 -  {
    1.33 -    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
    1.34 -  }
    1.35 -
    1.36 -
    1.37    /* protocol commands */
    1.38  
    1.39    def protocol_command_bytes(name: String, args: Bytes*): Unit
    1.40 @@ -311,7 +299,7 @@
    1.41    /* options */
    1.42  
    1.43    def options(opts: Options): Unit =
    1.44 -    protocol_command("Prover.options", YXML.string_of_body(opts.encode))
    1.45 +    protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
    1.46  
    1.47  
    1.48    /* interned items */
    1.49 @@ -327,10 +315,10 @@
    1.50        val encode_blob: T[Command.Blob] =
    1.51          variant(List(
    1.52            { case Exn.Res((a, b)) =>
    1.53 -              (Nil, pair(Encode.string, option(string))((a.node, b.map(p => p._1.toString)))) },
    1.54 -          { case Exn.Exn(e) => (Nil, Encode.string(Exn.message(e))) }))
    1.55 +              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    1.56 +          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    1.57  
    1.58 -      YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    1.59 +      Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    1.60      }
    1.61  
    1.62      val toks = command.span.content
    1.63 @@ -338,12 +326,12 @@
    1.64      {
    1.65        import XML.Encode._
    1.66        val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
    1.67 -      YXML.string_of_body(list(encode_tok)(toks))
    1.68 +      Symbol.encode_yxml(list(encode_tok)(toks))
    1.69      }
    1.70  
    1.71      protocol_command("Document.define_command",
    1.72 -      (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml ::
    1.73 -        toks.map(tok => encode(tok.source))): _*)
    1.74 +      (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
    1.75 +        toks.map(tok => Symbol.encode(tok.source))): _*)
    1.76    }
    1.77  
    1.78  
    1.79 @@ -374,20 +362,18 @@
    1.80                val theory = Long_Name.base_name(name.theory)
    1.81                val imports = header.imports.map({ case (a, _) => a.node })
    1.82                (Nil,
    1.83 -                pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
    1.84 -                  pair(list(pair(Encode.string,
    1.85 -                    pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
    1.86 -                  list(Encode.string)))))(
    1.87 +                pair(string, pair(string, pair(list(string), pair(list(pair(string,
    1.88 +                    pair(pair(string, list(string)), list(string)))), list(string)))))(
    1.89                  (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
    1.90            { case Document.Node.Perspective(a, b, c) =>
    1.91                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    1.92 -                list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
    1.93 +                list(pair(id, pair(string, list(string))))(c.dest)) }))
    1.94        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.95        {
    1.96          val (name, edit) = node_edit
    1.97 -        pair(Encode.string, encode_edit(name))(name.node, edit)
    1.98 +        pair(string, encode_edit(name))(name.node, edit)
    1.99        })
   1.100 -      YXML.string_of_body(encode_edits(edits)) }
   1.101 +      Symbol.encode_yxml(encode_edits(edits)) }
   1.102      protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   1.103    }
   1.104  
   1.105 @@ -395,7 +381,7 @@
   1.106    {
   1.107      val versions_yxml =
   1.108      { import XML.Encode._
   1.109 -      YXML.string_of_body(list(long)(versions.map(_.id))) }
   1.110 +      Symbol.encode_yxml(list(long)(versions.map(_.id))) }
   1.111      protocol_command("Document.remove_versions", versions_yxml)
   1.112    }
   1.113  
     2.1 --- a/src/Pure/PIDE/prover.scala	Sat Apr 01 19:17:15 2017 +0200
     2.2 +++ b/src/Pure/PIDE/prover.scala	Sat Apr 01 22:03:24 2017 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4  }
     2.5  
     2.6  
     2.7 -abstract class Prover(
     2.8 +class Prover(
     2.9    receiver: Prover.Receiver,
    2.10    xml_cache: XML.Cache,
    2.11    channel: System_Channel,
    2.12 @@ -232,7 +232,7 @@
    2.13              else done = true
    2.14            }
    2.15            if (result.length > 0) {
    2.16 -            output(markup, Nil, List(XML.Text(decode(result.toString))))
    2.17 +            output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
    2.18              result.length = 0
    2.19            }
    2.20            else {
    2.21 @@ -302,7 +302,7 @@
    2.22        def read_chunk(): XML.Body =
    2.23        {
    2.24          val (buf, n) = read_chunk_bytes()
    2.25 -        YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
    2.26 +        YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
    2.27        }
    2.28  
    2.29        try {
     3.1 --- a/src/Pure/System/isabelle_process.scala	Sat Apr 01 19:17:15 2017 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Apr 01 22:03:24 2017 +0200
     3.3 @@ -44,7 +44,7 @@
     3.4      receiver: Prover.Receiver = Console.println(_),
     3.5      xml_cache: XML.Cache = new XML.Cache(),
     3.6      tree: Option[Sessions.Tree] = None,
     3.7 -    store: Sessions.Store = Sessions.store()): Isabelle_Process =
     3.8 +    store: Sessions.Store = Sessions.store()): Prover =
     3.9    {
    3.10      val channel = System_Channel()
    3.11      val process =
    3.12 @@ -55,17 +55,6 @@
    3.13        catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    3.14      process.stdin.close
    3.15  
    3.16 -    new Isabelle_Process(receiver, xml_cache, channel, process)
    3.17 +    new Prover(receiver, xml_cache, channel, process)
    3.18    }
    3.19  }
    3.20 -
    3.21 -class Isabelle_Process private(
    3.22 -    receiver: Prover.Receiver,
    3.23 -    xml_cache: XML.Cache,
    3.24 -    channel: System_Channel,
    3.25 -    process: Bash.Process)
    3.26 -  extends Prover(receiver, xml_cache, channel, process)
    3.27 -{
    3.28 -  def encode(s: String): String = Symbol.encode(s)
    3.29 -  def decode(s: String): String = Symbol.decode(s)
    3.30 -}