# HG changeset patch # User wenzelm # Date 1426359096 -3600 # Node ID a03e0561bdbf3d6cb7a2fa7328cc924defa82cd1 # Parent d2bb4b5ed862dfe96c5abffd16286836e44e93d0 clarified positions of theory imports; diff -r d2bb4b5ed862 -r a03e0561bdbf src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/Isar/token.scala Sat Mar 14 19:51:36 2015 +0100 @@ -182,7 +182,7 @@ else new Pos(line1, offset1, file, id) } - def position(end_offset: Symbol.Offset): Position.T = + private 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) ::: @@ -204,7 +204,7 @@ def atEnd = tokens.isEmpty } - def reader(tokens: List[Token], file: String = "", id: Document_ID.Generic = Document_ID.none) + 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 d2bb4b5ed862 -r a03e0561bdbf src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/PIDE/document.scala Sat Mar 14 19:51:36 2015 +0100 @@ -81,7 +81,7 @@ /* header and name */ sealed case class Header( - imports: List[Name], + imports: List[(Name, Position.T)], keywords: Thy_Header.Keywords, errors: List[String]) { @@ -323,7 +323,7 @@ def + (entry: (Node.Name, Node)): Nodes = { val (name, node) = entry - val imports = node.header.imports + val imports = node.header.imports.map(_._1) val graph1 = (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty)) val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name)) diff -r d2bb4b5ed862 -r a03e0561bdbf src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/PIDE/protocol.scala Sat Mar 14 19:51:36 2015 +0100 @@ -433,7 +433,7 @@ { case Document.Node.Deps(header) => val master_dir = Isabelle_System.posix_path_url(name.master_dir) val theory = Long_Name.base_name(name.theory) - val imports = header.imports.map(_.node) + val imports = header.imports.map({ case (a, _) => a.node }) val keywords = header.keywords.map({ case (a, b, _) => (a, b) }) (Nil, pair(Encode.string, pair(Encode.string, pair(list(Encode.string), diff -r d2bb4b5ed862 -r a03e0561bdbf src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Mar 14 19:51:36 2015 +0100 @@ -91,7 +91,7 @@ { if (reader.source.length > 0) { try { - val header = Thy_Header.read(reader).decode_symbols + val header = Thy_Header.read(reader, node_name.node).decode_symbols val base_name = Long_Name.base_name(node_name.theory) val (name, pos) = header.name @@ -100,7 +100,7 @@ " for theory " + quote(name) + Position.here(pos)) val imports = - header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) }) + header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) }) Document.Node.Header(imports, header.keywords, Nil) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } diff -r d2bb4b5ed862 -r a03e0561bdbf src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/Thy/thy_header.scala Sat Mar 14 19:51:36 2015 +0100 @@ -124,7 +124,7 @@ /* read -- lazy scanning */ - def read(reader: Reader[Char]): Thy_Header = + def read(reader: Reader[Char], file: String): Thy_Header = { val token = Token.Parsers.token(bootstrap_keywords) val toks = new mutable.ListBuffer[Token] @@ -140,14 +140,14 @@ } scan_to_begin(reader) - parse(commit(header), Token.reader(toks.toList)) match { + parse(commit(header), Token.reader(toks.toList, file)) match { case Success(result, _) => result case bad => error(bad.toString) } } - def read(source: CharSequence): Thy_Header = - read(new CharSequenceReader(source)) + def read(source: CharSequence, file: String): Thy_Header = + read(new CharSequenceReader(source), file) } diff -r d2bb4b5ed862 -r a03e0561bdbf src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/Thy/thy_info.scala Sat Mar 14 19:51:36 2015 +0100 @@ -106,7 +106,7 @@ if (parent_loaded(dep.name.theory)) g else { val a = node(dep.name) - val bs = dep.header.imports.map(node _) + val bs = dep.header.imports.map({ case (name, _) => node(name) }) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) } } @@ -136,8 +136,7 @@ val header = try { resources.check_thy(session, name).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } - val imports = header.imports.map((_, Position.File(name.node))) - Dep(name, header) :: require_thys(session, name :: initiators, required1, imports) + Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports) } catch { case e: Throwable => diff -r d2bb4b5ed862 -r a03e0561bdbf src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Mar 14 18:18:40 2015 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Sat Mar 14 19:51:36 2015 +0100 @@ -82,7 +82,7 @@ node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header if (update_header) { val node1 = node.update_header(header) - if (node.header.imports != node1.header.imports || + if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) || node.header.keywords != node1.header.keywords) syntax_changed0 += name nodes += (name -> node1) doc_edits += (name -> Document.Node.Deps(header)) @@ -98,7 +98,7 @@ if (node.is_empty) None else { val header = node.header - val imports_syntax = header.imports.flatMap(a => nodes(a).syntax) + val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax) Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords)) } nodes += (name -> node.update_syntax(syntax))