# HG changeset patch # User wenzelm # Date 1491077004 -7200 # Node ID 2fdd4431b30ecec508ee398a6a952fd9cfd363aa # Parent b99283eed13c25582bad0bcb3b1152302dfc9abb clarified YXML vs. symbol encoding: operate on whole message; tuned signature; diff -r b99283eed13c -r 2fdd4431b30e src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Apr 01 19:17:15 2017 +0200 +++ b/src/Pure/PIDE/protocol.scala Sat Apr 01 22:03:24 2017 +0200 @@ -16,8 +16,7 @@ def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] = try { import XML.Decode._ - val body = YXML.parse_body(text) - Some(pair(long, list(pair(long, list(long))))(body)) + Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None @@ -30,7 +29,7 @@ def unapply(text: String): Option[List[Document_ID.Version]] = try { import XML.Decode._ - Some(list(long)(YXML.parse_body(text))) + Some(list(long)(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None @@ -291,17 +290,6 @@ trait Protocol { - /* text */ - - def encode(s: String): String - def decode(s: String): String - - object Encode - { - val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s))) - } - - /* protocol commands */ def protocol_command_bytes(name: String, args: Bytes*): Unit @@ -311,7 +299,7 @@ /* options */ def options(opts: Options): Unit = - protocol_command("Prover.options", YXML.string_of_body(opts.encode)) + protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) /* interned items */ @@ -327,10 +315,10 @@ val encode_blob: T[Command.Blob] = variant(List( { case Exn.Res((a, b)) => - (Nil, pair(Encode.string, option(string))((a.node, b.map(p => p._1.toString)))) }, - { case Exn.Exn(e) => (Nil, Encode.string(Exn.message(e))) })) + (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, + { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) - YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) + Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) } val toks = command.span.content @@ -338,12 +326,12 @@ { import XML.Encode._ val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) - YXML.string_of_body(list(encode_tok)(toks)) + Symbol.encode_yxml(list(encode_tok)(toks)) } protocol_command("Document.define_command", - (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml :: - toks.map(tok => encode(tok.source))): _*) + (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml :: + toks.map(tok => Symbol.encode(tok.source))): _*) } @@ -374,20 +362,18 @@ val theory = Long_Name.base_name(name.theory) val imports = header.imports.map({ case (a, _) => a.node }) (Nil, - pair(Encode.string, pair(Encode.string, pair(list(Encode.string), - pair(list(pair(Encode.string, - pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))), - list(Encode.string)))))( + pair(string, pair(string, pair(list(string), pair(list(pair(string, + pair(pair(string, list(string)), list(string)))), list(string)))))( (master_dir, (theory, (imports, (header.keywords, header.errors)))))) }, { case Document.Node.Perspective(a, b, c) => (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), - list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) })) + list(pair(id, pair(string, list(string))))(c.dest)) })) def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => { val (name, edit) = node_edit - pair(Encode.string, encode_edit(name))(name.node, edit) + pair(string, encode_edit(name))(name.node, edit) }) - YXML.string_of_body(encode_edits(edits)) } + Symbol.encode_yxml(encode_edits(edits)) } protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml) } @@ -395,7 +381,7 @@ { val versions_yxml = { import XML.Encode._ - YXML.string_of_body(list(long)(versions.map(_.id))) } + Symbol.encode_yxml(list(long)(versions.map(_.id))) } protocol_command("Document.remove_versions", versions_yxml) } diff -r b99283eed13c -r 2fdd4431b30e src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Sat Apr 01 19:17:15 2017 +0200 +++ b/src/Pure/PIDE/prover.scala Sat Apr 01 22:03:24 2017 +0200 @@ -62,7 +62,7 @@ } -abstract class Prover( +class Prover( receiver: Prover.Receiver, xml_cache: XML.Cache, channel: System_Channel, @@ -232,7 +232,7 @@ else done = true } if (result.length > 0) { - output(markup, Nil, List(XML.Text(decode(result.toString)))) + output(markup, Nil, List(XML.Text(Symbol.decode(result.toString)))) result.length = 0 } else { @@ -302,7 +302,7 @@ def read_chunk(): XML.Body = { val (buf, n) = read_chunk_bytes() - YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) + YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n)) } try { diff -r b99283eed13c -r 2fdd4431b30e src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Sat Apr 01 19:17:15 2017 +0200 +++ b/src/Pure/System/isabelle_process.scala Sat Apr 01 22:03:24 2017 +0200 @@ -44,7 +44,7 @@ receiver: Prover.Receiver = Console.println(_), xml_cache: XML.Cache = new XML.Cache(), tree: Option[Sessions.Tree] = None, - store: Sessions.Store = Sessions.store()): Isabelle_Process = + store: Sessions.Store = Sessions.store()): Prover = { val channel = System_Channel() val process = @@ -55,17 +55,6 @@ catch { case exn @ ERROR(_) => channel.accepted(); throw exn } process.stdin.close - new Isabelle_Process(receiver, xml_cache, channel, process) + new Prover(receiver, xml_cache, channel, process) } } - -class Isabelle_Process private( - receiver: Prover.Receiver, - xml_cache: XML.Cache, - channel: System_Channel, - process: Bash.Process) - extends Prover(receiver, xml_cache, channel, process) -{ - def encode(s: String): String = Symbol.encode(s) - def decode(s: String): String = Symbol.decode(s) -}