# HG changeset patch # User huffman # Date 1313532140 25200 # Node ID 17ae4af434aadcd753fd779460f067b3f448926d # Parent aa74ce315bae6d57a9bd673606711d81f95c0d5f# Parent d5f689c534c5cc64b18267f1ee171a962fbc0bd9 merged diff -r aa74ce315bae -r 17ae4af434aa Admin/update-keywords --- a/Admin/update-keywords Tue Aug 16 09:31:23 2011 -0700 +++ b/Admin/update-keywords Tue Aug 16 15:02:20 2011 -0700 @@ -12,7 +12,8 @@ isabelle keywords \ "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \ - "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" + "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \ + "$LOG/HOL-SPARK.gz" isabelle keywords -k ZF \ "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz" diff -r aa74ce315bae -r 17ae4af434aa etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Tue Aug 16 09:31:23 2011 -0700 +++ b/etc/isar-keywords-ZF.el Tue Aug 16 15:02:20 2011 -0700 @@ -40,12 +40,9 @@ "classrel" "codatatype" "code_datatype" - "code_library" - "code_module" "coinductive" "commit" "consts" - "consts_code" "context" "corollary" "datatype" @@ -194,7 +191,6 @@ "typed_print_translation" "typedecl" "types" - "types_code" "ultimately" "undo" "undos_proof" @@ -219,11 +215,9 @@ "case_eqns" "con_defs" "constrains" - "contains" "defines" "domains" "elimination" - "file" "fixes" "for" "identifier" @@ -354,11 +348,8 @@ "classrel" "codatatype" "code_datatype" - "code_library" - "code_module" "coinductive" "consts" - "consts_code" "context" "datatype" "declaration" @@ -410,7 +401,6 @@ "typed_print_translation" "typedecl" "types" - "types_code" "use")) (defconst isar-keywords-theory-script diff -r aa74ce315bae -r 17ae4af434aa etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Aug 16 09:31:23 2011 -0700 +++ b/etc/isar-keywords.el Tue Aug 16 15:02:20 2011 -0700 @@ -1,6 +1,6 @@ ;; ;; Keyword classification tables for Isabelle/Isar. -;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace + HOL-SPARK. +;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK. ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** ;; diff -r aa74ce315bae -r 17ae4af434aa src/Pure/General/position.ML --- a/src/Pure/General/position.ML Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Pure/General/position.ML Tue Aug 16 15:02:20 2011 -0700 @@ -171,7 +171,7 @@ (case (line_of pos, file_of pos) of (SOME i, NONE) => "(line " ^ string_of_int i ^ ")" | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")" - | (NONE, SOME name) => "(" ^ quote name ^ ")" + | (NONE, SOME name) => "(file " ^ quote name ^ ")" | _ => ""); in if null props then "" diff -r aa74ce315bae -r 17ae4af434aa src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Pure/PIDE/document.ML Tue Aug 16 15:02:20 2011 -0700 @@ -86,7 +86,6 @@ val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec)); fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; -fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; fun default_node name = Graph.default_node (name, empty_node); fun update_node name f = default_node name #> Graph.map_node name f; @@ -141,22 +140,19 @@ |> update_node name (edit_node edits) | Header header => let - val node = get_node nodes name; - val nodes' = Graph.new_node (name, node) (remove_node name nodes); - val parents = - (case header of Exn.Res (_, parents, _) => parents | _ => []) - |> filter (can (Graph.get_node nodes')); - val (header', nodes'') = - (header, Graph.add_deps_acyclic (name, parents) nodes') - handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes') - | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes') - in - nodes'' - |> Graph.map_node name (set_header header') - end)); + val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []); + val nodes1 = nodes + |> default_node name + |> fold default_node parents; + val nodes2 = nodes1 + |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); + val (header', nodes3) = + (header, Graph.add_deps_acyclic (name, parents) nodes2) + handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); + in Graph.map_node name (set_header header') nodes3 end)); -fun def_node name (Version nodes) = Version (default_node name nodes); -fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes); +fun put_node (name, node) (Version nodes) = + Version (update_node name (K node) nodes); end; @@ -331,10 +327,7 @@ let val old_version = the_version state old_id; val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) - val new_version = - old_version - |> fold (def_node o #1) edits - |> fold edit_nodes edits; + val new_version = fold edit_nodes edits old_version; val updates = nodes_of new_version |> Graph.schedule @@ -347,16 +340,17 @@ let val (thy_name, imports, uses) = Exn.release (get_header node); (* FIXME provide files via Scala layer *) - val dir = Path.dir (Path.explode name); - val files = map (apfst Path.explode) uses; + val (dir, files) = + if ML_System.platform_is_cygwin then (Path.current, []) + else (Path.dir (Path.explode name), map (apfst Path.explode) uses); val parents = imports |> map (fn import => - (case AList.lookup (op =) deps import of - SOME parent_future => - get_theory (Position.file_only (import ^ ".thy")) - (#2 (Future.join parent_future)) - | NONE => Thy_Info.get_theory (Thy_Info.base_name import))); + (case Thy_Info.lookup_theory import of + SOME thy => thy + | NONE => + get_theory (Position.file_only import) + (#2 (Future.join (the (AList.lookup (op =) deps import)))))); in Thy_Load.begin_theory dir thy_name imports files parents end fun get_command id = (id, the_command state id |> Future.map (Toplevel.modify_init init)); diff -r aa74ce315bae -r 17ae4af434aa src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Pure/PIDE/document.scala Tue Aug 16 15:02:20 2011 -0700 @@ -53,9 +53,9 @@ case class Edits[A](edits: List[A]) extends Edit[A] case class Header[A](header: Node_Header) extends Edit[A] - def norm_header[A](f: String => String, header: Node_Header): Header[A] = + def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] = header match { - case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) }) + case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) }) case exn => Header[A](exn) } diff -r aa74ce315bae -r 17ae4af434aa src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Pure/System/session.scala Tue Aug 16 15:02:20 2011 -0700 @@ -189,9 +189,15 @@ val syntax = current_syntax() val previous = global_state().history.tip.version - val norm_header = - Document.Node.norm_header[Text.Edit]( - name => file_store.append(master_dir, Path.explode(name)), header) + def norm_import(s: String): String = + { + val name = Thy_Header.base_name(s) + if (thy_load.is_loaded(name)) name + else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s))) + } + def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s)) + val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header) + val text_edits = (name, norm_header) :: edits.map(edit => (name, edit)) val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) } val change = diff -r aa74ce315bae -r 17ae4af434aa src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Pure/Thy/thy_header.scala Tue Aug 16 15:02:20 2011 -0700 @@ -28,11 +28,16 @@ /* theory file name */ - private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""") + private val Base_Name = new Regex(""".*?([^/\\:]+)""") + private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""") - def thy_name(s: String): Option[(String, String)] = - s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None } + def base_name(s: String): String = + s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) } + 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") def thy_path(name: String): Path = Path.basic(name).ext("thy") @@ -113,7 +118,7 @@ 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): Thy_Header = - copy(imports = imports.map(name => f(name)), uses = 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)), uses = uses.map(p => (g(p._1), p._2))) } diff -r aa74ce315bae -r 17ae4af434aa src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Pure/Thy/thy_info.ML Tue Aug 16 15:02:20 2011 -0700 @@ -9,7 +9,6 @@ sig datatype action = Update | Remove val add_hook: (action -> string -> unit) -> unit - val base_name: string -> string val get_names: unit -> string list val status: unit -> unit val lookup_theory: string -> theory option diff -r aa74ce315bae -r 17ae4af434aa src/Pure/Thy/thy_info.scala diff -r aa74ce315bae -r 17ae4af434aa src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Aug 16 09:31:23 2011 -0700 +++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 16 15:02:20 2011 -0700 @@ -190,9 +190,7 @@ { val master_dir = buffer.getDirectory val path = buffer.getSymlinkPath - if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS]) - (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path)) - else (master_dir, path) + (master_dir, path) } @@ -210,8 +208,8 @@ case None => val (master_dir, path) = buffer_path(buffer) Thy_Header.thy_name(path) match { - case Some((prefix, name)) => - Some(Document_Model.init(session, buffer, master_dir, prefix + name, name)) + case Some(name) => + Some(Document_Model.init(session, buffer, master_dir, path, name)) case None => None } } @@ -334,8 +332,8 @@ else { val vfs = VFSManager.getVFSForPath(master_dir) if (vfs.isInstanceOf[FileVFS]) - vfs.constructPath(master_dir, Isabelle_System.platform_path(path)) - // FIXME MiscUtilities.resolveSymlinks (!?) + MiscUtilities.resolveSymlinks( + vfs.constructPath(master_dir, Isabelle_System.platform_path(path))) else vfs.constructPath(master_dir, Isabelle_System.standard_path(path)) } }