clarified YXML vs. symbol encoding: operate on whole message;
authorwenzelm
Sat Apr 01 19:17:15 2017 +0200 (2017-04-01)
changeset 65344b99283eed13c
parent 65343 0a8e30a7b10e
child 65345 2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
src/Pure/General/completion.scala
src/Pure/General/symbol.scala
src/Pure/Thy/present.scala
src/Pure/Tools/build.scala
src/Pure/Tools/debugger.scala
src/Pure/Tools/print_operation.scala
     1.1 --- a/src/Pure/General/completion.scala	Sat Apr 01 19:16:19 2017 +0200
     1.2 +++ b/src/Pure/General/completion.scala	Sat Apr 01 19:17:15 2017 +0200
     1.3 @@ -70,8 +70,7 @@
     1.4          if (COMPLETION_HISTORY.is_file) {
     1.5            try {
     1.6              import XML.Decode._
     1.7 -            list(pair(Symbol.decode_string, int))(
     1.8 -              YXML.parse_body(File.read(COMPLETION_HISTORY)))
     1.9 +            list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
    1.10            }
    1.11            catch {
    1.12              case ERROR(msg) => ignore_error(msg); Nil
    1.13 @@ -110,7 +109,7 @@
    1.14        File.write_backup(COMPLETION_HISTORY,
    1.15          {
    1.16            import XML.Encode._
    1.17 -          YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
    1.18 +          Symbol.encode_yxml(list(pair(string, int))(rep.toList))
    1.19          })
    1.20      }
    1.21    }
     2.1 --- a/src/Pure/General/symbol.scala	Sat Apr 01 19:16:19 2017 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Sat Apr 01 19:17:15 2017 +0200
     2.3 @@ -506,8 +506,9 @@
     2.4    def decode(text: String): String = symbols.decode(text)
     2.5    def encode(text: String): String = symbols.encode(text)
     2.6  
     2.7 -  def decode_string: XML.Decode.T[String] = (x => decode(XML.Decode.string(x)))
     2.8 -  def encode_string: XML.Encode.T[String] = (x => XML.Encode.string(encode(x)))
     2.9 +  def decode_yxml(text: String): XML.Body = YXML.parse_body(decode(text))
    2.10 +  def decode_yxml_failsafe(text: String): XML.Body = YXML.parse_body_failsafe(decode(text))
    2.11 +  def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
    2.12  
    2.13    def decode_strict(text: String): String =
    2.14    {
     3.1 --- a/src/Pure/Thy/present.scala	Sat Apr 01 19:16:19 2017 +0200
     3.2 +++ b/src/Pure/Thy/present.scala	Sat Apr 01 19:17:15 2017 +0200
     3.3 @@ -50,7 +50,7 @@
     3.4      val path = dir + sessions_path
     3.5      if (path.is_file) {
     3.6        import XML.Decode._
     3.7 -      list(pair(string, string))(YXML.parse_body(File.read(path)))
     3.8 +      list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
     3.9      }
    3.10      else Nil
    3.11    }
     4.1 --- a/src/Pure/Tools/build.scala	Sat Apr 01 19:16:19 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Sat Apr 01 19:17:15 2017 +0200
     4.3 @@ -142,7 +142,7 @@
     4.4      private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
     4.5      {
     4.6        val error_message =
     4.7 -        try { Pretty.string_of(YXML.parse_body(Symbol.decode(msg.text))) }
     4.8 +        try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
     4.9          catch { case ERROR(msg) => msg }
    4.10        result_error.fulfill(error_message)
    4.11        session.send_stop()
     5.1 --- a/src/Pure/Tools/debugger.scala	Sat Apr 01 19:16:19 2017 +0200
     5.2 +++ b/src/Pure/Tools/debugger.scala	Sat Apr 01 19:17:15 2017 +0200
     5.3 @@ -112,12 +112,11 @@
     5.4      {
     5.5        msg.properties match {
     5.6          case Markup.Debugger_State(thread_name) =>
     5.7 -          val msg_body =
     5.8 -            YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
     5.9 +          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
    5.10            val debug_states =
    5.11            {
    5.12              import XML.Decode._
    5.13 -            list(pair(properties, Symbol.decode_string))(msg_body).map({
    5.14 +            list(pair(properties, string))(msg_body).map({
    5.15                case (pos, function) => Debug_State(pos, function)
    5.16              })
    5.17            }
    5.18 @@ -131,7 +130,7 @@
    5.19      {
    5.20        msg.properties match {
    5.21          case Markup.Debugger_Output(thread_name) =>
    5.22 -          YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
    5.23 +          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
    5.24              case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
    5.25                val message = XML.Elem(Markup(Markup.message(name), props), body)
    5.26                debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
     6.1 --- a/src/Pure/Tools/print_operation.scala	Sat Apr 01 19:16:19 2017 +0200
     6.2 +++ b/src/Pure/Tools/print_operation.scala	Sat Apr 01 19:17:15 2017 +0200
     6.3 @@ -32,7 +32,7 @@
     6.4        val ops =
     6.5        {
     6.6          import XML.Decode._
     6.7 -        list(pair(string, string))(YXML.parse_body(msg.text))
     6.8 +        list(pair(string, string))(Symbol.decode_yxml(msg.text))
     6.9        }
    6.10        print_operations.change(_ => ops)
    6.11        true