more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
authorwenzelm
Tue Mar 10 20:12:30 2015 +0100 (2015-03-10)
changeset 596719715eb8e9408
parent 59666 0e9f303d1515
child 59672 4028c156136a
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
src/Pure/GUI/gui.scala
src/Pure/General/output.scala
src/Pure/General/position.scala
src/Pure/Isar/parse.scala
src/Pure/Isar/token.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Tue Mar 10 13:55:10 2015 +0100
     1.2 +++ b/src/Pure/GUI/gui.scala	Tue Mar 10 20:12:30 2015 +0100
     1.3 @@ -80,9 +80,10 @@
     1.4  
     1.5    /* simple dialogs */
     1.6  
     1.7 -  def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
     1.8 +  def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
     1.9      : ScrollPane =
    1.10    {
    1.11 +    val txt = Output.clean_yxml(raw_txt)
    1.12      val text = new TextArea(txt)
    1.13      if (width > 0) text.columns = width
    1.14      if (height > 0 && split_lines(txt).length > height) text.rows = height
     2.1 --- a/src/Pure/General/output.scala	Tue Mar 10 13:55:10 2015 +0100
     2.2 +++ b/src/Pure/General/output.scala	Tue Mar 10 20:12:30 2015 +0100
     2.3 @@ -10,11 +10,15 @@
     2.4  
     2.5  object Output
     2.6  {
     2.7 -  def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
     2.8 -  def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
     2.9 +  def clean_yxml(msg: String): String =
    2.10 +    try { XML.content(YXML.parse_body(msg)) }
    2.11 +    catch { case ERROR(_) => msg }
    2.12  
    2.13 -  def writeln(msg: String) { Console.err.println(msg) }
    2.14 +  def writeln_text(msg: String): String = clean_yxml(msg)
    2.15 +  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
    2.16 +  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
    2.17 +
    2.18 +  def writeln(msg: String) { Console.err.println(writeln_text(msg)) }
    2.19    def warning(msg: String) { Console.err.println(warning_text(msg)) }
    2.20    def error_message(msg: String) { Console.err.println(error_text(msg)) }
    2.21  }
    2.22 -
     3.1 --- a/src/Pure/General/position.scala	Tue Mar 10 13:55:10 2015 +0100
     3.2 +++ b/src/Pure/General/position.scala	Tue Mar 10 20:12:30 2015 +0100
     3.3 @@ -101,19 +101,24 @@
     3.4  
     3.5    /* here: user output */
     3.6  
     3.7 +  def yxml_markup(pos: T, str: String): String =
     3.8 +    YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str))))
     3.9 +
    3.10    def here(pos: T): String =
    3.11 -    (Line.unapply(pos), File.unapply(pos)) match {
    3.12 -      case (Some(i), None) => " (line " + i.toString + ")"
    3.13 -      case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
    3.14 -      case (None, Some(name)) => " (file " + quote(name) + ")"
    3.15 -      case _ => ""
    3.16 -    }
    3.17 +    yxml_markup(pos,
    3.18 +      (Line.unapply(pos), File.unapply(pos)) match {
    3.19 +        case (Some(i), None) => " (line " + i.toString + ")"
    3.20 +        case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
    3.21 +        case (None, Some(name)) => " (file " + quote(name) + ")"
    3.22 +        case _ => ""
    3.23 +      })
    3.24  
    3.25    def here_undelimited(pos: T): String =
    3.26 -    (Line.unapply(pos), File.unapply(pos)) match {
    3.27 -      case (Some(i), None) => "line " + i.toString
    3.28 -      case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
    3.29 -      case (None, Some(name)) => "file " + quote(name)
    3.30 -      case _ => ""
    3.31 -    }
    3.32 +    yxml_markup(pos,
    3.33 +      (Line.unapply(pos), File.unapply(pos)) match {
    3.34 +        case (Some(i), None) => "line " + i.toString
    3.35 +        case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
    3.36 +        case (None, Some(name)) => "file " + quote(name)
    3.37 +        case _ => ""
    3.38 +      })
    3.39  }
     4.1 --- a/src/Pure/Isar/parse.scala	Tue Mar 10 13:55:10 2015 +0100
     4.2 +++ b/src/Pure/Isar/parse.scala	Tue Mar 10 20:12:30 2015 +0100
     4.3 @@ -49,7 +49,7 @@
     4.4  
     4.5      def command(name: String): Parser[Position.T] =
     4.6        token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
     4.7 -        { case (_, pos) => pos.position }
     4.8 +        { case (tok, pos) => pos.position(tok) }
     4.9  
    4.10      def $$$(name: String): Parser[String] =
    4.11        atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
     5.1 --- a/src/Pure/Isar/token.scala	Tue Mar 10 13:55:10 2015 +0100
     5.2 +++ b/src/Pure/Isar/token.scala	Tue Mar 10 20:12:30 2015 +0100
     5.3 @@ -157,10 +157,14 @@
     5.4  
     5.5    object Pos
     5.6    {
     5.7 -    val none: Pos = new Pos(0, "")
     5.8 +    val none: Pos = new Pos()
     5.9    }
    5.10  
    5.11 -  final class Pos private[Token](val line: Int, val file: String)
    5.12 +  final class Pos private[Token](
    5.13 +      val line: Int = 0,
    5.14 +      val offset: Symbol.Offset = 0,
    5.15 +      val file: String = "",
    5.16 +      val id: Document_ID.Generic = Document_ID.none)
    5.17      extends scala.util.parsing.input.Position
    5.18    {
    5.19      def column = 0
    5.20 @@ -168,13 +172,27 @@
    5.21  
    5.22      def advance(token: Token): Pos =
    5.23      {
    5.24 -      var n = 0
    5.25 -      for (c <- token.content if c == '\n') n += 1
    5.26 -      if (n == 0) this else new Pos(line + n, file)
    5.27 +      var line1 = line
    5.28 +      var offset1 = offset
    5.29 +      for (s <- Symbol.iterator(token.source)) {
    5.30 +        if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
    5.31 +        if (offset1 > 0) offset1 += 1
    5.32 +      }
    5.33 +      if (line1 == line && offset1 == offset) this
    5.34 +      else new Pos(line1, offset1, file, id)
    5.35      }
    5.36  
    5.37 -    def position: Position.T = Position.Line_File(line, file)
    5.38 -    override def toString: String = Position.here_undelimited(position)
    5.39 +    def position(end_offset: Symbol.Offset): Position.T =
    5.40 +      (if (line > 0) Position.Line(line) else Nil) :::
    5.41 +      (if (offset > 0) Position.Offset(offset) else Nil) :::
    5.42 +      (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
    5.43 +      (if (file != "") Position.File(file) else Nil) :::
    5.44 +      (if (id != Document_ID.none) Position.Id(id) else Nil)
    5.45 +
    5.46 +    def position(): Position.T = position(0)
    5.47 +    def position(token: Token): Position.T = position(advance(token).offset)
    5.48 +
    5.49 +    override def toString: String = Position.here_undelimited(position())
    5.50    }
    5.51  
    5.52    abstract class Reader extends scala.util.parsing.input.Reader[Token]
    5.53 @@ -186,8 +204,8 @@
    5.54      def atEnd = tokens.isEmpty
    5.55    }
    5.56  
    5.57 -  def reader(tokens: List[Token], file: String = ""): Reader =
    5.58 -    new Token_Reader(tokens, new Pos(1, file))
    5.59 +  def reader(tokens: List[Token], file: String = "", id: Document_ID.Generic = Document_ID.none)
    5.60 +    : Reader = new Token_Reader(tokens, new Pos(1, 1, file, id))
    5.61  }
    5.62  
    5.63  
     6.1 --- a/src/Pure/PIDE/protocol.ML	Tue Mar 10 13:55:10 2015 +0100
     6.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Mar 10 20:12:30 2015 +0100
     6.3 @@ -35,7 +35,7 @@
     6.4              let open XML.Decode in
     6.5                list (variant
     6.6                 [fn ([], a) => Exn.Res (pair string (option string) a),
     6.7 -                fn ([], a) => Exn.Exn (ERROR (string a))])
     6.8 +                fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
     6.9              end;
    6.10          val toks =
    6.11            (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
    6.12 @@ -72,7 +72,7 @@
    6.13                            pair string (pair string (pair (list string)
    6.14                              (pair (list (pair string
    6.15                                (option (pair (pair string (list string)) (list string)))))
    6.16 -                              (list string)))) a;
    6.17 +                              (list YXML.string_of_body)))) a;
    6.18                          val imports' = map (rpair Position.none) imports;
    6.19                          val header = Thy_Header.make (name, Position.none) imports' keywords;
    6.20                        in Document.Deps (master, header, errors) end,
     7.1 --- a/src/Pure/PIDE/protocol.scala	Tue Mar 10 13:55:10 2015 +0100
     7.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 10 20:12:30 2015 +0100
     7.3 @@ -382,7 +382,7 @@
     7.4    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     7.5      protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
     7.6  
     7.7 -  def define_command(command: Command): Unit =
     7.8 +  def define_command(command: Command)
     7.9    {
    7.10      val blobs_yxml =
    7.11      { import XML.Encode._