clarified positions of theory imports;
authorwenzelm
Sat Mar 14 19:51:36 2015 +0100 (2015-03-14)
changeset 59695a03e0561bdbf
parent 59694 d2bb4b5ed862
child 59696 f505fee04400
clarified positions of theory imports;
src/Pure/Isar/token.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/token.scala	Sat Mar 14 18:18:40 2015 +0100
     1.2 +++ b/src/Pure/Isar/token.scala	Sat Mar 14 19:51:36 2015 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4        else new Pos(line1, offset1, file, id)
     1.5      }
     1.6  
     1.7 -    def position(end_offset: Symbol.Offset): Position.T =
     1.8 +    private def position(end_offset: Symbol.Offset): Position.T =
     1.9        (if (line > 0) Position.Line(line) else Nil) :::
    1.10        (if (offset > 0) Position.Offset(offset) else Nil) :::
    1.11        (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
    1.12 @@ -204,7 +204,7 @@
    1.13      def atEnd = tokens.isEmpty
    1.14    }
    1.15  
    1.16 -  def reader(tokens: List[Token], file: String = "", id: Document_ID.Generic = Document_ID.none)
    1.17 +  def reader(tokens: List[Token], file: String, id: Document_ID.Generic = Document_ID.none)
    1.18      : Reader = new Token_Reader(tokens, new Pos(1, 1, file, id))
    1.19  }
    1.20  
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 14 18:18:40 2015 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 14 19:51:36 2015 +0100
     2.3 @@ -81,7 +81,7 @@
     2.4      /* header and name */
     2.5  
     2.6      sealed case class Header(
     2.7 -      imports: List[Name],
     2.8 +      imports: List[(Name, Position.T)],
     2.9        keywords: Thy_Header.Keywords,
    2.10        errors: List[String])
    2.11      {
    2.12 @@ -323,7 +323,7 @@
    2.13      def + (entry: (Node.Name, Node)): Nodes =
    2.14      {
    2.15        val (name, node) = entry
    2.16 -      val imports = node.header.imports
    2.17 +      val imports = node.header.imports.map(_._1)
    2.18        val graph1 =
    2.19          (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
    2.20        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
     3.1 --- a/src/Pure/PIDE/protocol.scala	Sat Mar 14 18:18:40 2015 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Mar 14 19:51:36 2015 +0100
     3.3 @@ -433,7 +433,7 @@
     3.4            { case Document.Node.Deps(header) =>
     3.5                val master_dir = Isabelle_System.posix_path_url(name.master_dir)
     3.6                val theory = Long_Name.base_name(name.theory)
     3.7 -              val imports = header.imports.map(_.node)
     3.8 +              val imports = header.imports.map({ case (a, _) => a.node })
     3.9                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
    3.10                (Nil,
    3.11                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
     4.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 14 18:18:40 2015 +0100
     4.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 14 19:51:36 2015 +0100
     4.3 @@ -91,7 +91,7 @@
     4.4    {
     4.5      if (reader.source.length > 0) {
     4.6        try {
     4.7 -        val header = Thy_Header.read(reader).decode_symbols
     4.8 +        val header = Thy_Header.read(reader, node_name.node).decode_symbols
     4.9  
    4.10          val base_name = Long_Name.base_name(node_name.theory)
    4.11          val (name, pos) = header.name
    4.12 @@ -100,7 +100,7 @@
    4.13              " for theory " + quote(name) + Position.here(pos))
    4.14  
    4.15          val imports =
    4.16 -          header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) })
    4.17 +          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
    4.18          Document.Node.Header(imports, header.keywords, Nil)
    4.19        }
    4.20        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     5.1 --- a/src/Pure/Thy/thy_header.scala	Sat Mar 14 18:18:40 2015 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Mar 14 19:51:36 2015 +0100
     5.3 @@ -124,7 +124,7 @@
     5.4  
     5.5    /* read -- lazy scanning */
     5.6  
     5.7 -  def read(reader: Reader[Char]): Thy_Header =
     5.8 +  def read(reader: Reader[Char], file: String): Thy_Header =
     5.9    {
    5.10      val token = Token.Parsers.token(bootstrap_keywords)
    5.11      val toks = new mutable.ListBuffer[Token]
    5.12 @@ -140,14 +140,14 @@
    5.13      }
    5.14      scan_to_begin(reader)
    5.15  
    5.16 -    parse(commit(header), Token.reader(toks.toList)) match {
    5.17 +    parse(commit(header), Token.reader(toks.toList, file)) match {
    5.18        case Success(result, _) => result
    5.19        case bad => error(bad.toString)
    5.20      }
    5.21    }
    5.22  
    5.23 -  def read(source: CharSequence): Thy_Header =
    5.24 -    read(new CharSequenceReader(source))
    5.25 +  def read(source: CharSequence, file: String): Thy_Header =
    5.26 +    read(new CharSequenceReader(source), file)
    5.27  }
    5.28  
    5.29  
     6.1 --- a/src/Pure/Thy/thy_info.scala	Sat Mar 14 18:18:40 2015 +0100
     6.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Mar 14 19:51:36 2015 +0100
     6.3 @@ -106,7 +106,7 @@
     6.4            if (parent_loaded(dep.name.theory)) g
     6.5            else {
     6.6              val a = node(dep.name)
     6.7 -            val bs = dep.header.imports.map(node _)
     6.8 +            val bs = dep.header.imports.map({ case (name, _) => node(name) })
     6.9              ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    6.10            }
    6.11        }
    6.12 @@ -136,8 +136,7 @@
    6.13          val header =
    6.14            try { resources.check_thy(session, name).cat_errors(message) }
    6.15            catch { case ERROR(msg) => cat_error(msg, message) }
    6.16 -        val imports = header.imports.map((_, Position.File(name.node)))
    6.17 -        Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
    6.18 +        Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
    6.19        }
    6.20        catch {
    6.21          case e: Throwable =>
     7.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 14 18:18:40 2015 +0100
     7.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 14 19:51:36 2015 +0100
     7.3 @@ -82,7 +82,7 @@
     7.4            node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
     7.5          if (update_header) {
     7.6            val node1 = node.update_header(header)
     7.7 -          if (node.header.imports != node1.header.imports ||
     7.8 +          if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
     7.9                node.header.keywords != node1.header.keywords) syntax_changed0 += name
    7.10            nodes += (name -> node1)
    7.11            doc_edits += (name -> Document.Node.Deps(header))
    7.12 @@ -98,7 +98,7 @@
    7.13          if (node.is_empty) None
    7.14          else {
    7.15            val header = node.header
    7.16 -          val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
    7.17 +          val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
    7.18            Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
    7.19          }
    7.20        nodes += (name -> node.update_syntax(syntax))