proper command id for inlined errors, which is important for Command.State.accumulate;
authorwenzelm
Sun Mar 15 21:57:10 2015 +0100 (2015-03-15)
changeset 59706bf6ca55aae13
parent 59705 740a0ca7e09b
child 59707 10effab11669
proper command id for inlined errors, which is important for Command.State.accumulate;
src/Pure/General/position.scala
src/Pure/Isar/token.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/General/position.scala	Sun Mar 15 20:35:47 2015 +0100
     1.2 +++ b/src/Pure/General/position.scala	Sun Mar 15 21:57:10 2015 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4    val End_Offset = new Properties.Int(Markup.END_OFFSET)
     1.5    val File = new Properties.String(Markup.FILE)
     1.6    val Id = new Properties.Long(Markup.ID)
     1.7 +  val Id_String = new Properties.String(Markup.ID)
     1.8  
     1.9    val Def_Line = new Properties.Int(Markup.DEF_LINE)
    1.10    val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
     2.1 --- a/src/Pure/Isar/token.scala	Sun Mar 15 20:35:47 2015 +0100
     2.2 +++ b/src/Pure/Isar/token.scala	Sun Mar 15 21:57:10 2015 +0100
     2.3 @@ -157,16 +157,17 @@
     2.4  
     2.5    object Pos
     2.6    {
     2.7 -    val none: Pos = new Pos(0, 0, "")
     2.8 -    val start: Pos = new Pos(1, 1, "")
     2.9 -    val offset: Pos = new Pos(0, 1, "")
    2.10 -    def file(file: String): Pos = new Pos(1, 1, file)
    2.11 +    val none: Pos = new Pos(0, 0, "", "")
    2.12 +    val start: Pos = new Pos(1, 1, "", "")
    2.13 +    def file(file: String): Pos = new Pos(1, 1, file, "")
    2.14 +    def id(id: String): Pos = new Pos(0, 1, "", id)
    2.15    }
    2.16  
    2.17    final class Pos private[Token](
    2.18        val line: Int,
    2.19        val offset: Symbol.Offset,
    2.20 -      val file: String)
    2.21 +      val file: String,
    2.22 +      val id: String)
    2.23      extends scala.util.parsing.input.Position
    2.24    {
    2.25      def column = 0
    2.26 @@ -181,14 +182,15 @@
    2.27          if (offset1 > 0) offset1 += 1
    2.28        }
    2.29        if (line1 == line && offset1 == offset) this
    2.30 -      else new Pos(line1, offset1, file)
    2.31 +      else new Pos(line1, offset1, file, id)
    2.32      }
    2.33  
    2.34      private def position(end_offset: Symbol.Offset): Position.T =
    2.35        (if (line > 0) Position.Line(line) else Nil) :::
    2.36        (if (offset > 0) Position.Offset(offset) else Nil) :::
    2.37        (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
    2.38 -      (if (file != "") Position.File(file) else Nil)
    2.39 +      (if (file != "") Position.File(file) else Nil) :::
    2.40 +      (if (id != "") Position.Id_String(id) else Nil)
    2.41  
    2.42      def position(): Position.T = position(0)
    2.43      def position(token: Token): Position.T = position(advance(token).offset)
     3.1 --- a/src/Pure/PIDE/command.scala	Sun Mar 15 20:35:47 2015 +0100
     3.2 +++ b/src/Pure/PIDE/command.scala	Sun Mar 15 21:57:10 2015 +0100
     3.3 @@ -362,7 +362,7 @@
     3.4        case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
     3.5          val header =
     3.6            resources.check_thy_reader("", node_name,
     3.7 -            new CharSequenceReader(span.source), Token.Pos.offset)
     3.8 +            new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
     3.9          val import_errors =
    3.10            for ((imp, pos) <- header.imports if !can_import(imp))
    3.11              yield "Bad theory import " + quote(imp.node) + Position.here(pos)
     4.1 --- a/src/Pure/PIDE/protocol.scala	Sun Mar 15 20:35:47 2015 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Mar 15 21:57:10 2015 +0100
     4.3 @@ -382,6 +382,29 @@
     4.4    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     4.5      protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
     4.6  
     4.7 +  private def resolve_id(id: String, body: XML.Body): XML.Body =
     4.8 +  {
     4.9 +    def resolve_property(p: (String, String)): (String, String) =
    4.10 +      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
    4.11 +
    4.12 +    def resolve_markup(markup: Markup): Markup =
    4.13 +      Markup(markup.name, markup.properties.map(resolve_property))
    4.14 +
    4.15 +    def resolve_tree(t: XML.Tree): XML.Tree =
    4.16 +      t match {
    4.17 +        case XML.Wrapped_Elem(markup, ts1, ts2) =>
    4.18 +          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
    4.19 +        case XML.Elem(markup, ts) =>
    4.20 +          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
    4.21 +        case text => text
    4.22 +      }
    4.23 +    body.map(resolve_tree _)
    4.24 +  }
    4.25 +
    4.26 +  private def resolve_id(id: String, s: String): XML.Body =
    4.27 +    try { resolve_id(id, YXML.parse_body(s)) }
    4.28 +    catch { case ERROR(_) => XML.Encode.string(s) }
    4.29 +
    4.30    def define_command(command: Command)
    4.31    {
    4.32      val blobs_yxml =
    4.33 @@ -390,7 +413,7 @@
    4.34          variant(List(
    4.35            { case Exn.Res((a, b)) =>
    4.36                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    4.37 -          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    4.38 +          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
    4.39  
    4.40        YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    4.41      }