--- a/src/Pure/GUI/gui.scala Tue Mar 10 17:50:10 2015 +0100
+++ b/src/Pure/GUI/gui.scala Tue Mar 10 20:12:34 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 17:50:10 2015 +0100
+++ b/src/Pure/General/output.scala Tue Mar 10 20:12:34 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 17:50:10 2015 +0100
+++ b/src/Pure/General/position.scala Tue Mar 10 20:12:34 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 17:50:10 2015 +0100
+++ b/src/Pure/Isar/parse.scala Tue Mar 10 20:12:34 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 17:50:10 2015 +0100
+++ b/src/Pure/Isar/token.scala Tue Mar 10 20:12:34 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 17:50:10 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML Tue Mar 10 20:12:34 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 17:50:10 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Mar 10 20:12:34 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._