# HG changeset patch # User wenzelm # Date 1426014750 -3600 # Node ID 9715eb8e9408cbdd92c752e11bd4567721ab4e82 # Parent 0e9f303d151524aca91b2a24d51be7aa6c6ad090 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/GUI/gui.scala --- 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 diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/General/output.scala --- 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)) } } - diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/General/position.scala --- 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 _ => "" + }) } diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/Isar/parse.scala --- 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) diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/Isar/token.scala --- 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)) } diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/PIDE/protocol.ML --- 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, diff -r 0e9f303d1515 -r 9715eb8e9408 src/Pure/PIDE/protocol.scala --- 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._