more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;

--- a/src/Pure/GUI/gui.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -80,9 +80,10 @@
 
   /* simple dialogs */
 
-  def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
+  def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
     : ScrollPane =
   {
+    val txt = Output.clean_yxml(raw_txt)
     val text = new TextArea(txt)
     if (width > 0) text.columns = width
     if (height > 0 && split_lines(txt).length > height) text.rows = height

--- a/src/Pure/General/output.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/General/output.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -10,11 +10,15 @@
 
 object Output
 {
-  def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
-  def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+  def clean_yxml(msg: String): String =
+    try { XML.content(YXML.parse_body(msg)) }
+    catch { case ERROR(_) => msg }
 
-  def writeln(msg: String) { Console.err.println(msg) }
+  def writeln_text(msg: String): String = clean_yxml(msg)
+  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
+  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
+
+  def writeln(msg: String) { Console.err.println(writeln_text(msg)) }
   def warning(msg: String) { Console.err.println(warning_text(msg)) }
   def error_message(msg: String) { Console.err.println(error_text(msg)) }
 }
-

--- a/src/Pure/General/position.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/General/position.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -101,19 +101,24 @@
 
   /* here: user output */
 
+  def yxml_markup(pos: T, str: String): String =
+    YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str))))
+
   def here(pos: T): String =
-    (Line.unapply(pos), File.unapply(pos)) match {
-      case (Some(i), None) => " (line " + i.toString + ")"
-      case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
-      case (None, Some(name)) => " (file " + quote(name) + ")"
-      case _ => ""
-    }
+    yxml_markup(pos,
+      (Line.unapply(pos), File.unapply(pos)) match {
+        case (Some(i), None) => " (line " + i.toString + ")"
+        case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
+        case (None, Some(name)) => " (file " + quote(name) + ")"
+        case _ => ""
+      })
 
   def here_undelimited(pos: T): String =
-    (Line.unapply(pos), File.unapply(pos)) match {
-      case (Some(i), None) => "line " + i.toString
-      case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
-      case (None, Some(name)) => "file " + quote(name)
-      case _ => ""
-    }
+    yxml_markup(pos,
+      (Line.unapply(pos), File.unapply(pos)) match {
+        case (Some(i), None) => "line " + i.toString
+        case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
+        case (None, Some(name)) => "file " + quote(name)
+        case _ => ""
+      })
 }

--- a/src/Pure/Isar/parse.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/Isar/parse.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -49,7 +49,7 @@
 
     def command(name: String): Parser[Position.T] =
       token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
-        { case (_, pos) => pos.position }
+        { case (tok, pos) => pos.position(tok) }
 
     def $$$(name: String): Parser[String] =
       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)

--- a/src/Pure/Isar/token.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/Isar/token.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -157,10 +157,14 @@
 
   object Pos
   {
-    val none: Pos = new Pos(0, "")
+    val none: Pos = new Pos()
   }
 
-  final class Pos private[Token](val line: Int, val file: String)
+  final class Pos private[Token](
+      val line: Int = 0,
+      val offset: Symbol.Offset = 0,
+      val file: String = "",
+      val id: Document_ID.Generic = Document_ID.none)
     extends scala.util.parsing.input.Position
   {
     def column = 0
@@ -168,13 +172,27 @@
 
     def advance(token: Token): Pos =
     {
-      var n = 0
-      for (c <- token.content if c == '\n') n += 1
-      if (n == 0) this else new Pos(line + n, file)
+      var line1 = line
+      var offset1 = offset
+      for (s <- Symbol.iterator(token.source)) {
+        if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
+        if (offset1 > 0) offset1 += 1
+      }
+      if (line1 == line && offset1 == offset) this
+      else new Pos(line1, offset1, file, id)
     }
 
-    def position: Position.T = Position.Line_File(line, file)
-    override def toString: String = Position.here_undelimited(position)
+    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 (id != Document_ID.none) Position.Id(id) else Nil)
+
+    def position(): Position.T = position(0)
+    def position(token: Token): Position.T = position(advance(token).offset)
+
+    override def toString: String = Position.here_undelimited(position())
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]
@@ -186,8 +204,8 @@
     def atEnd = tokens.isEmpty
   }
 
-  def reader(tokens: List[Token], file: String = ""): Reader =
-    new Token_Reader(tokens, new Pos(1, file))
+  def reader(tokens: List[Token], file: String = "", id: Document_ID.Generic = Document_ID.none)
+    : Reader = new Token_Reader(tokens, new Pos(1, 1, file, id))
 }
 
 

--- a/src/Pure/PIDE/protocol.ML	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Tue Mar 10 20:12:30 2015 +0100
@@ -35,7 +35,7 @@
             let open XML.Decode in
               list (variant
                [fn ([], a) => Exn.Res (pair string (option string) a),
-                fn ([], a) => Exn.Exn (ERROR (string a))])
+                fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
             end;
         val toks =
           (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
@@ -72,7 +72,7 @@
                           pair string (pair string (pair (list string)
                             (pair (list (pair string
                               (option (pair (pair string (list string)) (list string)))))
-                              (list string)))) a;
+                              (list YXML.string_of_body)))) a;
                         val imports' = map (rpair Position.none) imports;
                         val header = Thy_Header.make (name, Position.none) imports' keywords;
                       in Document.Deps (master, header, errors) end,

--- a/src/Pure/PIDE/protocol.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -382,7 +382,7 @@
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
 
-  def define_command(command: Command): Unit =
+  def define_command(command: Command)
   {
     val blobs_yxml =
     { import XML.Encode._