# HG changeset patch # User wenzelm # Date 1330553346 -3600 # Node ID 09ab89658a5d783f7f662da88ef02e0e9eed31b4 # Parent 4dc7ddb473501188b41b6fb071762ba19c2961b0 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies; diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/PIDE/document.scala Wed Feb 29 23:09:06 2012 +0100 @@ -35,10 +35,12 @@ type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective] - type Node_Header = Exn.Result[Thy_Header] + type Node_Header = Exn.Result[Node.Deps] object Node { + sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)]) + object Name { val empty = Name("", "", "") @@ -81,12 +83,6 @@ case class Header[A, B](header: Node_Header) extends Edit[A, B] case class Perspective[A, B](perspective: B) extends Edit[A, B] - def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header = - header match { - case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) } - case exn => exn - } - def command_starts(commands: Iterator[Command], offset: Text.Offset = 0) : Iterator[(Command, Text.Offset)] = { @@ -194,9 +190,7 @@ val (name, node) = entry val parents = node.header match { - case Exn.Res(header) => - // FIXME official names of yet unknown nodes!? - for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name + case Exn.Res(deps) => deps.imports.filter(_.dir != "") // FIXME more specific filter case _ => Nil } val graph1 = diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/PIDE/protocol.scala Wed Feb 29 23:09:06 2012 +0100 @@ -211,22 +211,24 @@ val edits_yxml = { import XML.Encode._ def id: T[Command] = (cmd => long(cmd.id)) - def encode_edit(dir: String) + def encode_edit(name: Document.Node.Name) : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = variant(List( { case Document.Node.Clear() => (Nil, Nil) }, { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, - { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => + { case Document.Node.Header(Exn.Res(deps)) => + val dir = Isabelle_System.posix_path(name.dir) + val imports = deps.imports.map(_.node) + val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) (Nil, triple(pair(string, string), list(string), list(pair(string, bool)))( - (dir, a), b, c)) }, + (dir, name.theory), imports, uses)) }, { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => { val (name, edit) = node_edit - val dir = Isabelle_System.posix_path(name.dir) - pair(string, encode_edit(dir))(name.node, edit) + pair(string, encode_edit(name))(name.node, edit) }) YXML.string_of_body(encode(edits)) } input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml) diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Feb 29 23:09:06 2012 +0100 @@ -143,7 +143,7 @@ Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ())) handle ERROR msg => (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); - tell_file_retracted (Thy_Header.thy_path name)) + tell_file_retracted (Thy_Load.thy_path (Path.basic name))) val _ = Isar.init (); in () end; diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/System/session.scala Wed Feb 29 23:09:06 2012 +0100 @@ -35,7 +35,7 @@ } -class Session(thy_load: Thy_Load = new Thy_Load) +class Session(val thy_load: Thy_Load = new Thy_Load) { /* real time parameters */ // FIXME properties or settings (!?) @@ -143,20 +143,11 @@ def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text = { - def norm_import(s: String): String = - { - val thy_name = Thy_Header.base_name(s) - if (thy_load.is_loaded(thy_name)) thy_name - else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s))) - } - def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s)) - val header1: Document.Node_Header = header match { - case Exn.Res(Thy_Header(thy_name, _, _)) - if (thy_load.is_loaded(thy_name)) => - Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name))) - case _ => Document.Node.norm_header(norm_import, norm_use, header) + case Exn.Res(_) if (thy_load.is_loaded(name.theory)) => + Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory))) + case _ => header } (name, Document.Node.Header(header1)) } diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/Thy/thy_header.ML Wed Feb 29 23:09:06 2012 +0100 @@ -8,8 +8,6 @@ sig val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list val read: Position.T -> string -> string * string list * (Path.T * bool) list - val thy_path: string -> Path.T - val consistent_name: string -> string -> unit end; structure Thy_Header: THY_HEADER = @@ -67,13 +65,4 @@ | NONE => error ("Unexpected end of input" ^ Position.str_of pos)) end; - -(* file name *) - -val thy_path = Path.ext "thy" o Path.basic; - -fun consistent_name name name' = - if name = name' then () - else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name'); - end; diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/Thy/thy_header.scala Wed Feb 29 23:09:06 2012 +0100 @@ -37,8 +37,6 @@ def thy_name(s: String): Option[String] = s match { case Thy_Name(name) => Some(name) case _ => None } - def thy_path(path: Path): Path = path.ext("thy") - /* header */ @@ -96,18 +94,6 @@ try { read(reader).map(Standard_System.decode_permissive_utf8) } finally { reader.close } } - - - /* check */ - - def check(name: String, source: CharSequence): Thy_Header = - { - val header = read(source) - val name1 = header.name - val path = Path.explode(name) - if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1)) - header - } } @@ -116,10 +102,5 @@ { def map(f: String => String): Thy_Header = Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2))) - - def norm_deps(f: String => String, g: String => String): Thy_Header = - copy(imports = imports.map(name => f(name))) - // FIXME - // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2))) } diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/Thy/thy_info.scala Wed Feb 29 23:09:06 2012 +0100 @@ -24,15 +24,6 @@ /* dependencies */ - def import_name(dir: String, str: String): Document.Node.Name = - { - val path = Path.explode(str) - val node = thy_load.append(dir, Thy_Header.thy_path(path)) - val dir1 = thy_load.append(dir, path.dir) - val theory = path.base.implode - Document.Node.Name(node, dir1, theory) - } - type Dep = (Document.Node.Name, Document.Node_Header) private type Required = (List[Dep], Set[Document.Node.Name]) @@ -49,16 +40,16 @@ else { try { if (initiators.contains(name)) error(cycle_msg(initiators)) - val header = + val node_deps = try { thy_load.check_thy(name) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred while examining theory " + quote(name.theory) + required_by(initiators)) } - val imports = header.imports.map(import_name(name.dir, _)) - val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports) - ((name, Exn.Res(header)) :: deps1, seen1) + val (deps1, seen1) = + require_thys(name :: initiators, (deps, seen + name), node_deps.imports) + ((name, Exn.Res(node_deps)) :: deps1, seen1) } catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) } } diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/Thy/thy_load.ML Wed Feb 29 23:09:06 2012 +0100 @@ -10,6 +10,7 @@ val imports_of: theory -> string list val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory val check_file: Path.T -> Path.T -> Path.T + val thy_path: Path.T -> Path.T val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list} val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string @@ -75,14 +76,18 @@ fun check_file dir file = File.check_file (File.full_path dir file); +val thy_path = Path.ext "thy"; + fun check_thy dir name = let - val master_file = check_file dir (Thy_Header.thy_path name); + val path = thy_path (Path.basic name); + val master_file = check_file dir path; val text = File.read master_file; val (name', imports, uses) = if name = Context.PureN then (Context.PureN, [], []) else Thy_Header.read (Path.position master_file) text; - val _ = Thy_Header.consistent_name name name'; + val _ = name <> name' andalso + error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name'); in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end; diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/Thy/thy_load.scala Wed Feb 29 23:09:06 2012 +0100 @@ -29,11 +29,39 @@ def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).implode - def check_thy(name: Document.Node.Name): Thy_Header = + def read_header(name: Document.Node.Name): Thy_Header = { val file = new File(name.node) if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) Thy_Header.read(file) } + + + /* theory files */ + + def thy_path(path: Path): Path = path.ext("thy") + + private def import_name(dir: String, s: String): Document.Node.Name = + { + val theory = Thy_Header.base_name(s) + if (is_loaded(theory)) Document.Node.Name(theory, "", theory) + else { + val path = Path.explode(s) + val node = append(dir, thy_path(path)) + val dir1 = append(dir, path.dir) + Document.Node.Name(node, dir1, theory) + } + } + + def check_thy(name: Document.Node.Name): Document.Node.Deps = + { + val header = read_header(name) + val name1 = header.name + val imports = header.imports.map(import_name(name.dir, _)) + val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) + if (name.theory != name1) + error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1)) + Document.Node.Deps(imports, uses) + } } diff -r 4dc7ddb47350 -r 09ab89658a5d src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Wed Feb 29 23:09:06 2012 +0100 @@ -258,7 +258,7 @@ val node = nodes(name) val update_header = (node.header, header) match { - case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header + case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps case _ => true } if (update_header) { diff -r 4dc7ddb47350 -r 09ab89658a5d src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Tools/Code/code_runtime.ML Wed Feb 29 23:09:06 2012 +0100 @@ -310,8 +310,9 @@ | process_reflection (code, _) _ (SOME file_name) thy = let val preamble = - "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy)) - ^ "; DO NOT EDIT! *)"; + "(* Generated from " ^ + Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^ + "; DO NOT EDIT! *)"; val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); in thy diff -r 4dc7ddb47350 -r 09ab89658a5d src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Wed Feb 29 23:09:06 2012 +0100 @@ -60,10 +60,11 @@ { /* header */ - def node_header(): Exn.Result[Thy_Header] = + def node_header(): Document.Node_Header = { Swing_Thread.require() - Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) } + // FIXME assert(Isabelle.jedit_buffer(name.node) == Some(buffer)) + Exn.capture { session.thy_load.check_thy(name) } } diff -r 4dc7ddb47350 -r 09ab89658a5d src/Tools/jEdit/src/jedit_thy_load.scala --- a/src/Tools/jEdit/src/jedit_thy_load.scala Wed Feb 29 17:43:41 2012 +0100 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala Wed Feb 29 23:09:06 2012 +0100 @@ -52,7 +52,7 @@ } } - override def check_thy(name: Document.Node.Name): Thy_Header = + override def read_header(name: Document.Node.Name): Thy_Header = { Swing_Thread.now { Isabelle.jedit_buffer(name.node) match {