--- 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"
--- 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
--- 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 ***
;;
--- 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 ""
--- 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));
--- 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)
}
--- 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 =
--- 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)))
}
--- 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
--- 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))
}
}