# HG changeset patch
# User wenzelm
# Date 1426453030 -3600
# Node ID bf6ca55aae13c9248b5f9cd76bbd352dbd6129b2
# Parent  740a0ca7e09b6ad976faa198ecc94482985193a3
proper command id for inlined errors, which is important for Command.State.accumulate;

diff -r 740a0ca7e09b -r bf6ca55aae13 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sun Mar 15 20:35:47 2015 +0100
+++ b/src/Pure/General/position.scala	Sun Mar 15 21:57:10 2015 +0100
@@ -21,6 +21,7 @@
   val End_Offset = new Properties.Int(Markup.END_OFFSET)
   val File = new Properties.String(Markup.FILE)
   val Id = new Properties.Long(Markup.ID)
+  val Id_String = new Properties.String(Markup.ID)
 
   val Def_Line = new Properties.Int(Markup.DEF_LINE)
   val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
diff -r 740a0ca7e09b -r bf6ca55aae13 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sun Mar 15 20:35:47 2015 +0100
+++ b/src/Pure/Isar/token.scala	Sun Mar 15 21:57:10 2015 +0100
@@ -157,16 +157,17 @@
 
   object Pos
   {
-    val none: Pos = new Pos(0, 0, "")
-    val start: Pos = new Pos(1, 1, "")
-    val offset: Pos = new Pos(0, 1, "")
-    def file(file: String): Pos = new Pos(1, 1, file)
+    val none: Pos = new Pos(0, 0, "", "")
+    val start: Pos = new Pos(1, 1, "", "")
+    def file(file: String): Pos = new Pos(1, 1, file, "")
+    def id(id: String): Pos = new Pos(0, 1, "", id)
   }
 
   final class Pos private[Token](
       val line: Int,
       val offset: Symbol.Offset,
-      val file: String)
+      val file: String,
+      val id: String)
     extends scala.util.parsing.input.Position
   {
     def column = 0
@@ -181,14 +182,15 @@
         if (offset1 > 0) offset1 += 1
       }
       if (line1 == line && offset1 == offset) this
-      else new Pos(line1, offset1, file)
+      else new Pos(line1, offset1, file, id)
     }
 
     private def position(end_offset: Symbol.Offset): Position.T =
       (if (line > 0) Position.Line(line) else Nil) :::
       (if (offset > 0) Position.Offset(offset) else Nil) :::
       (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
-      (if (file != "") Position.File(file) else Nil)
+      (if (file != "") Position.File(file) else Nil) :::
+      (if (id != "") Position.Id_String(id) else Nil)
 
     def position(): Position.T = position(0)
     def position(token: Token): Position.T = position(advance(token).offset)
diff -r 740a0ca7e09b -r bf6ca55aae13 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Mar 15 20:35:47 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 15 21:57:10 2015 +0100
@@ -362,7 +362,7 @@
       case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
         val header =
           resources.check_thy_reader("", node_name,
-            new CharSequenceReader(span.source), Token.Pos.offset)
+            new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
         val import_errors =
           for ((imp, pos) <- header.imports if !can_import(imp))
             yield "Bad theory import " + quote(imp.node) + Position.here(pos)
diff -r 740a0ca7e09b -r bf6ca55aae13 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Mar 15 20:35:47 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Mar 15 21:57:10 2015 +0100
@@ -382,6 +382,29 @@
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
 
+  private def resolve_id(id: String, body: XML.Body): XML.Body =
+  {
+    def resolve_property(p: (String, String)): (String, String) =
+      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
+
+    def resolve_markup(markup: Markup): Markup =
+      Markup(markup.name, markup.properties.map(resolve_property))
+
+    def resolve_tree(t: XML.Tree): XML.Tree =
+      t match {
+        case XML.Wrapped_Elem(markup, ts1, ts2) =>
+          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
+        case XML.Elem(markup, ts) =>
+          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
+        case text => text
+      }
+    body.map(resolve_tree _)
+  }
+
+  private def resolve_id(id: String, s: String): XML.Body =
+    try { resolve_id(id, YXML.parse_body(s)) }
+    catch { case ERROR(_) => XML.Encode.string(s) }
+
   def define_command(command: Command)
   {
     val blobs_yxml =
@@ -390,7 +413,7 @@
         variant(List(
           { case Exn.Res((a, b)) =>
               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
-          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
 
       YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }