clarified span position;
authorwenzelm
Sun Mar 15 20:35:47 2015 +0100 (2015-03-15)
changeset 59705740a0ca7e09b
parent 59704 b5eb7c688836
child 59706 bf6ca55aae13
clarified span position;
src/Pure/Isar/token.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/resources.scala
src/Pure/System/options.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/Isar/token.scala	Sun Mar 15 19:48:49 2015 +0100
     1.2 +++ b/src/Pure/Isar/token.scala	Sun Mar 15 20:35:47 2015 +0100
     1.3 @@ -158,7 +158,9 @@
     1.4    object Pos
     1.5    {
     1.6      val none: Pos = new Pos(0, 0, "")
     1.7 -    def file(file: String): Pos = new Pos(0, 0, file)
     1.8 +    val start: Pos = new Pos(1, 1, "")
     1.9 +    val offset: Pos = new Pos(0, 1, "")
    1.10 +    def file(file: String): Pos = new Pos(1, 1, file)
    1.11    }
    1.12  
    1.13    final class Pos private[Token](
    1.14 @@ -203,8 +205,8 @@
    1.15      def atEnd = tokens.isEmpty
    1.16    }
    1.17  
    1.18 -  def reader(tokens: List[Token], file: String): Reader =
    1.19 -    new Token_Reader(tokens, Pos.file(file))
    1.20 +  def reader(tokens: List[Token], start: Token.Pos): Reader =
    1.21 +    new Token_Reader(tokens, start)
    1.22  }
    1.23  
    1.24  
     2.1 --- a/src/Pure/PIDE/command.scala	Sun Mar 15 19:48:49 2015 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Sun Mar 15 20:35:47 2015 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4  
     2.5  import scala.collection.mutable
     2.6  import scala.collection.immutable.SortedMap
     2.7 +import scala.util.parsing.input.CharSequenceReader
     2.8  
     2.9  
    2.10  object Command
    2.11 @@ -354,12 +355,14 @@
    2.12      get_blob: Document.Node.Name => Option[Document.Blob],
    2.13      can_import: Document.Node.Name => Boolean,
    2.14      node_name: Document.Node.Name,
    2.15 -    header: Document.Node.Header,
    2.16      span: Command_Span.Span): Blobs_Info =
    2.17    {
    2.18      span.kind match {
    2.19        // inlined errors
    2.20        case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
    2.21 +        val header =
    2.22 +          resources.check_thy_reader("", node_name,
    2.23 +            new CharSequenceReader(span.source), Token.Pos.offset)
    2.24          val import_errors =
    2.25            for ((imp, pos) <- header.imports if !can_import(imp))
    2.26              yield "Bad theory import " + quote(imp.node) + Position.here(pos)
     3.1 --- a/src/Pure/PIDE/command_span.scala	Sun Mar 15 19:48:49 2015 +0100
     3.2 +++ b/src/Pure/PIDE/command_span.scala	Sun Mar 15 20:35:47 2015 +0100
     3.3 @@ -28,23 +28,24 @@
     3.4    {
     3.5      def length: Int = (0 /: content)(_ + _.source.length)
     3.6  
     3.7 +    def source: String =
     3.8 +      content match {
     3.9 +        case List(tok) => tok.source
    3.10 +        case toks => toks.map(_.source).mkString
    3.11 +      }
    3.12 +
    3.13      def compact_source: (String, Span) =
    3.14      {
    3.15 -      val source: String =
    3.16 -        content match {
    3.17 -          case List(tok) => tok.source
    3.18 -          case toks => toks.map(_.source).mkString
    3.19 -        }
    3.20 -
    3.21 +      val src = source
    3.22        val content1 = new mutable.ListBuffer[Token]
    3.23        var i = 0
    3.24        for (Token(kind, s) <- content) {
    3.25          val n = s.length
    3.26 -        val s1 = source.substring(i, i + n)
    3.27 +        val s1 = src.substring(i, i + n)
    3.28          content1 += Token(kind, s1)
    3.29          i += n
    3.30        }
    3.31 -      (source, Span(kind, content1.toList))
    3.32 +      (src, Span(kind, content1.toList))
    3.33      }
    3.34    }
    3.35  
     4.1 --- a/src/Pure/PIDE/resources.scala	Sun Mar 15 19:48:49 2015 +0100
     4.2 +++ b/src/Pure/PIDE/resources.scala	Sun Mar 15 20:35:47 2015 +0100
     4.3 @@ -86,12 +86,12 @@
     4.4      }
     4.5    }
     4.6  
     4.7 -  def check_thy_reader(qualifier: String, node_name: Document.Node.Name, reader: Reader[Char])
     4.8 -    : Document.Node.Header =
     4.9 +  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
    4.10 +    reader: Reader[Char], start: Token.Pos): Document.Node.Header =
    4.11    {
    4.12      if (reader.source.length > 0) {
    4.13        try {
    4.14 -        val header = Thy_Header.read(reader, node_name.node).decode_symbols
    4.15 +        val header = Thy_Header.read(reader, start).decode_symbols
    4.16  
    4.17          val base_name = Long_Name.base_name(node_name.theory)
    4.18          val (name, pos) = header.name
    4.19 @@ -108,8 +108,9 @@
    4.20      else Document.Node.no_header
    4.21    }
    4.22  
    4.23 -  def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
    4.24 -    with_thy_reader(name, check_thy_reader(qualifier, name, _))
    4.25 +  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
    4.26 +    : Document.Node.Header =
    4.27 +    with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
    4.28  
    4.29    def check_file(file: String): Boolean =
    4.30      try {
     5.1 --- a/src/Pure/System/options.scala	Sun Mar 15 19:48:49 2015 +0100
     5.2 +++ b/src/Pure/System/options.scala	Sun Mar 15 20:35:47 2015 +0100
     5.3 @@ -110,7 +110,7 @@
     5.4      {
     5.5        val toks = Token.explode(syntax.keywords, File.read(file))
     5.6        val ops =
     5.7 -        parse_all(rep(parser), Token.reader(toks, file.implode)) match {
     5.8 +        parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
     5.9            case Success(result, _) => result
    5.10            case bad => error(bad.toString)
    5.11          }
     6.1 --- a/src/Pure/Thy/thy_header.scala	Sun Mar 15 19:48:49 2015 +0100
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Mar 15 20:35:47 2015 +0100
     6.3 @@ -124,7 +124,7 @@
     6.4  
     6.5    /* read -- lazy scanning */
     6.6  
     6.7 -  def read(reader: Reader[Char], file: String): Thy_Header =
     6.8 +  def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
     6.9    {
    6.10      val token = Token.Parsers.token(bootstrap_keywords)
    6.11      val toks = new mutable.ListBuffer[Token]
    6.12 @@ -140,14 +140,14 @@
    6.13      }
    6.14      scan_to_begin(reader)
    6.15  
    6.16 -    parse(commit(header), Token.reader(toks.toList, file)) match {
    6.17 +    parse(commit(header), Token.reader(toks.toList, start)) match {
    6.18        case Success(result, _) => result
    6.19        case bad => error(bad.toString)
    6.20      }
    6.21    }
    6.22  
    6.23 -  def read(source: CharSequence, file: String): Thy_Header =
    6.24 -    read(new CharSequenceReader(source), file)
    6.25 +  def read(source: CharSequence, start: Token.Pos): Thy_Header =
    6.26 +    read(new CharSequenceReader(source), start)
    6.27  }
    6.28  
    6.29  
     7.1 --- a/src/Pure/Thy/thy_info.scala	Sun Mar 15 19:48:49 2015 +0100
     7.2 +++ b/src/Pure/Thy/thy_info.scala	Sun Mar 15 20:35:47 2015 +0100
     7.3 @@ -134,7 +134,7 @@
     7.4        try {
     7.5          if (initiators.contains(name)) error(cycle_msg(initiators))
     7.6          val header =
     7.7 -          try { resources.check_thy(session, name).cat_errors(message) }
     7.8 +          try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
     7.9            catch { case ERROR(msg) => cat_error(msg, message) }
    7.10          Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
    7.11        }
     8.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 19:48:49 2015 +0100
     8.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 20:35:47 2015 +0100
     8.3 @@ -159,15 +159,13 @@
     8.4      get_blob: Document.Node.Name => Option[Document.Blob],
     8.5      can_import: Document.Node.Name => Boolean,
     8.6      node_name: Document.Node.Name,
     8.7 -    header: Document.Node.Header,
     8.8      commands: Linear_Set[Command],
     8.9      first: Command, last: Command): Linear_Set[Command] =
    8.10    {
    8.11      val cmds0 = commands.iterator(first, last).toList
    8.12      val blobs_spans0 =
    8.13        syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
    8.14 -        (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, header, span),
    8.15 -          span))
    8.16 +        (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, span), span))
    8.17  
    8.18      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    8.19  
    8.20 @@ -213,7 +211,6 @@
    8.21      // FIXME somewhat slow
    8.22      def recover_spans(
    8.23        name: Document.Node.Name,
    8.24 -      header: Document.Node.Header,
    8.25        perspective: Command.Perspective,
    8.26        commands: Linear_Set[Command]): Linear_Set[Command] =
    8.27      {
    8.28 @@ -229,7 +226,7 @@
    8.29              val first = next_invisible(cmds.reverse, first_unparsed)
    8.30              val last = next_invisible(cmds, first_unparsed)
    8.31              recover(
    8.32 -              reparse_spans(resources, syntax, get_blob, can_import, name, header, cmds, first, last))
    8.33 +              reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
    8.34            case None => cmds
    8.35          }
    8.36        recover(commands)
    8.37 @@ -244,7 +241,7 @@
    8.38          if (name.is_theory) {
    8.39            val commands0 = node.commands
    8.40            val commands1 = edit_text(text_edits, commands0)
    8.41 -          val commands2 = recover_spans(name, node.header, node.perspective.visible, commands1)
    8.42 +          val commands2 = recover_spans(name, node.perspective.visible, commands1)
    8.43            node.update_commands(commands2)
    8.44          }
    8.45          else node
    8.46 @@ -274,8 +271,8 @@
    8.47                          last = it.next
    8.48                          i += last.length
    8.49                        }
    8.50 -                      reparse_spans(resources, syntax, get_blob, can_import, name,
    8.51 -                        node.header, commands, first_unfinished, last)
    8.52 +                      reparse_spans(resources, syntax, get_blob, can_import,
    8.53 +                        name, commands, first_unfinished, last)
    8.54                      case None => commands
    8.55                    }
    8.56                  case None => commands
    8.57 @@ -330,7 +327,7 @@
    8.58                if (reparse_set(name) && commands.nonEmpty)
    8.59                  node.update_commands(
    8.60                    reparse_spans(resources, syntax, get_blob, can_import, name,
    8.61 -                    node.header, commands, commands.head, commands.last))
    8.62 +                    commands, commands.head, commands.last))
    8.63                else node
    8.64              val node2 =
    8.65                (node1 /: edits)(
     9.1 --- a/src/Pure/Tools/build.scala	Sun Mar 15 19:48:49 2015 +0100
     9.2 +++ b/src/Pure/Tools/build.scala	Sun Mar 15 20:35:47 2015 +0100
     9.3 @@ -260,8 +260,9 @@
     9.4      def parse_entries(root: Path): List[(String, Session_Entry)] =
     9.5      {
     9.6        val toks = Token.explode(root_syntax.keywords, File.read(root))
     9.7 +      val start = Token.Pos.file(root.implode)
     9.8  
     9.9 -      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
    9.10 +      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
    9.11          case Success(result, _) =>
    9.12            var chapter = chapter_default
    9.13            val entries = new mutable.ListBuffer[(String, Session_Entry)]
    10.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Mar 15 19:48:49 2015 +0100
    10.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Mar 15 20:35:47 2015 +0100
    10.3 @@ -79,7 +79,8 @@
    10.4      if (is_theory) {
    10.5        JEdit_Lib.buffer_lock(buffer) {
    10.6          Exn.capture {
    10.7 -          PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
    10.8 +          PIDE.resources.check_thy_reader("", node_name,
    10.9 +            JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
   10.10          } match {
   10.11            case Exn.Res(header) => header
   10.12            case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))