merged
authorhuffman
Tue Aug 16 15:02:20 2011 -0700 (2011-08-16)
changeset 4423417ae4af434aa
parent 44233 aa74ce315bae
parent 44232 d5f689c534c5
child 44235 85e9dad3c187
merged
     1.1 --- a/Admin/update-keywords	Tue Aug 16 09:31:23 2011 -0700
     1.2 +++ b/Admin/update-keywords	Tue Aug 16 15:02:20 2011 -0700
     1.3 @@ -12,7 +12,8 @@
     1.4  
     1.5  isabelle keywords \
     1.6    "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
     1.7 -  "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz"
     1.8 +  "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
     1.9 +  "$LOG/HOL-SPARK.gz"
    1.10  
    1.11  isabelle keywords -k ZF \
    1.12    "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
     2.1 --- a/etc/isar-keywords-ZF.el	Tue Aug 16 09:31:23 2011 -0700
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Aug 16 15:02:20 2011 -0700
     2.3 @@ -40,12 +40,9 @@
     2.4      "classrel"
     2.5      "codatatype"
     2.6      "code_datatype"
     2.7 -    "code_library"
     2.8 -    "code_module"
     2.9      "coinductive"
    2.10      "commit"
    2.11      "consts"
    2.12 -    "consts_code"
    2.13      "context"
    2.14      "corollary"
    2.15      "datatype"
    2.16 @@ -194,7 +191,6 @@
    2.17      "typed_print_translation"
    2.18      "typedecl"
    2.19      "types"
    2.20 -    "types_code"
    2.21      "ultimately"
    2.22      "undo"
    2.23      "undos_proof"
    2.24 @@ -219,11 +215,9 @@
    2.25      "case_eqns"
    2.26      "con_defs"
    2.27      "constrains"
    2.28 -    "contains"
    2.29      "defines"
    2.30      "domains"
    2.31      "elimination"
    2.32 -    "file"
    2.33      "fixes"
    2.34      "for"
    2.35      "identifier"
    2.36 @@ -354,11 +348,8 @@
    2.37      "classrel"
    2.38      "codatatype"
    2.39      "code_datatype"
    2.40 -    "code_library"
    2.41 -    "code_module"
    2.42      "coinductive"
    2.43      "consts"
    2.44 -    "consts_code"
    2.45      "context"
    2.46      "datatype"
    2.47      "declaration"
    2.48 @@ -410,7 +401,6 @@
    2.49      "typed_print_translation"
    2.50      "typedecl"
    2.51      "types"
    2.52 -    "types_code"
    2.53      "use"))
    2.54  
    2.55  (defconst isar-keywords-theory-script
     3.1 --- a/etc/isar-keywords.el	Tue Aug 16 09:31:23 2011 -0700
     3.2 +++ b/etc/isar-keywords.el	Tue Aug 16 15:02:20 2011 -0700
     3.3 @@ -1,6 +1,6 @@
     3.4  ;;
     3.5  ;; Keyword classification tables for Isabelle/Isar.
     3.6 -;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace + HOL-SPARK.
     3.7 +;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK.
     3.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     3.9  ;;
    3.10  
     4.1 --- a/src/Pure/General/position.ML	Tue Aug 16 09:31:23 2011 -0700
     4.2 +++ b/src/Pure/General/position.ML	Tue Aug 16 15:02:20 2011 -0700
     4.3 @@ -171,7 +171,7 @@
     4.4        (case (line_of pos, file_of pos) of
     4.5          (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
     4.6        | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
     4.7 -      | (NONE, SOME name) => "(" ^ quote name ^ ")"
     4.8 +      | (NONE, SOME name) => "(file " ^ quote name ^ ")"
     4.9        | _ => "");
    4.10    in
    4.11      if null props then ""
     5.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 16 09:31:23 2011 -0700
     5.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 16 15:02:20 2011 -0700
     5.3 @@ -86,7 +86,6 @@
     5.4  val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
     5.5  
     5.6  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
     5.7 -fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
     5.8  fun default_node name = Graph.default_node (name, empty_node);
     5.9  fun update_node name f = default_node name #> Graph.map_node name f;
    5.10  
    5.11 @@ -141,22 +140,19 @@
    5.12            |> update_node name (edit_node edits)
    5.13        | Header header =>
    5.14            let
    5.15 -            val node = get_node nodes name;
    5.16 -            val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    5.17 -            val parents =
    5.18 -              (case header of Exn.Res (_, parents, _) => parents | _ => [])
    5.19 -              |> filter (can (Graph.get_node nodes'));
    5.20 -            val (header', nodes'') =
    5.21 -              (header, Graph.add_deps_acyclic (name, parents) nodes')
    5.22 -                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
    5.23 -                  | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
    5.24 -          in
    5.25 -            nodes''
    5.26 -            |> Graph.map_node name (set_header header')
    5.27 -          end));
    5.28 +            val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
    5.29 +            val nodes1 = nodes
    5.30 +              |> default_node name
    5.31 +              |> fold default_node parents;
    5.32 +            val nodes2 = nodes1
    5.33 +              |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    5.34 +            val (header', nodes3) =
    5.35 +              (header, Graph.add_deps_acyclic (name, parents) nodes2)
    5.36 +                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    5.37 +          in Graph.map_node name (set_header header') nodes3 end));
    5.38  
    5.39 -fun def_node name (Version nodes) = Version (default_node name nodes);
    5.40 -fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
    5.41 +fun put_node (name, node) (Version nodes) =
    5.42 +  Version (update_node name (K node) nodes);
    5.43  
    5.44  end;
    5.45  
    5.46 @@ -331,10 +327,7 @@
    5.47    let
    5.48      val old_version = the_version state old_id;
    5.49      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
    5.50 -    val new_version =
    5.51 -      old_version
    5.52 -      |> fold (def_node o #1) edits
    5.53 -      |> fold edit_nodes edits;
    5.54 +    val new_version = fold edit_nodes edits old_version;
    5.55  
    5.56      val updates =
    5.57        nodes_of new_version |> Graph.schedule
    5.58 @@ -347,16 +340,17 @@
    5.59                    let
    5.60                      val (thy_name, imports, uses) = Exn.release (get_header node);
    5.61                      (* FIXME provide files via Scala layer *)
    5.62 -                    val dir = Path.dir (Path.explode name);
    5.63 -                    val files = map (apfst Path.explode) uses;
    5.64 +                    val (dir, files) =
    5.65 +                      if ML_System.platform_is_cygwin then (Path.current, [])
    5.66 +                      else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
    5.67  
    5.68                      val parents =
    5.69                        imports |> map (fn import =>
    5.70 -                        (case AList.lookup (op =) deps import of
    5.71 -                          SOME parent_future =>
    5.72 -                            get_theory (Position.file_only (import ^ ".thy"))
    5.73 -                              (#2 (Future.join parent_future))
    5.74 -                        | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
    5.75 +                        (case Thy_Info.lookup_theory import of
    5.76 +                          SOME thy => thy
    5.77 +                        | NONE =>
    5.78 +                            get_theory (Position.file_only import)
    5.79 +                              (#2 (Future.join (the (AList.lookup (op =) deps import))))));
    5.80                    in Thy_Load.begin_theory dir thy_name imports files parents end
    5.81                  fun get_command id =
    5.82                    (id, the_command state id |> Future.map (Toplevel.modify_init init));
     6.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 16 09:31:23 2011 -0700
     6.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 16 15:02:20 2011 -0700
     6.3 @@ -53,9 +53,9 @@
     6.4      case class Edits[A](edits: List[A]) extends Edit[A]
     6.5      case class Header[A](header: Node_Header) extends Edit[A]
     6.6  
     6.7 -    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
     6.8 +    def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
     6.9        header match {
    6.10 -        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
    6.11 +        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
    6.12          case exn => Header[A](exn)
    6.13        }
    6.14  
     7.1 --- a/src/Pure/System/session.scala	Tue Aug 16 09:31:23 2011 -0700
     7.2 +++ b/src/Pure/System/session.scala	Tue Aug 16 15:02:20 2011 -0700
     7.3 @@ -189,9 +189,15 @@
     7.4        val syntax = current_syntax()
     7.5        val previous = global_state().history.tip.version
     7.6  
     7.7 -      val norm_header =
     7.8 -        Document.Node.norm_header[Text.Edit](
     7.9 -          name => file_store.append(master_dir, Path.explode(name)), header)
    7.10 +      def norm_import(s: String): String =
    7.11 +      {
    7.12 +        val name = Thy_Header.base_name(s)
    7.13 +        if (thy_load.is_loaded(name)) name
    7.14 +        else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    7.15 +      }
    7.16 +      def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
    7.17 +      val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header)
    7.18 +
    7.19        val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    7.20        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
    7.21        val change =
     8.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 16 09:31:23 2011 -0700
     8.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 16 15:02:20 2011 -0700
     8.3 @@ -28,11 +28,16 @@
     8.4  
     8.5    /* theory file name */
     8.6  
     8.7 -  private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
     8.8 +  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
     8.9 +  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    8.10  
    8.11 -  def thy_name(s: String): Option[(String, String)] =
    8.12 -    s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
    8.13 +  def base_name(s: String): String =
    8.14 +    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    8.15  
    8.16 +  def thy_name(s: String): Option[String] =
    8.17 +    s match { case Thy_Name(name) => Some(name) case _ => None }
    8.18 +
    8.19 +  def thy_path(path: Path): Path = path.ext("thy")
    8.20    def thy_path(name: String): Path = Path.basic(name).ext("thy")
    8.21  
    8.22  
    8.23 @@ -113,7 +118,7 @@
    8.24    def map(f: String => String): Thy_Header =
    8.25      Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
    8.26  
    8.27 -  def norm_deps(f: String => String): Thy_Header =
    8.28 -    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
    8.29 +  def norm_deps(f: String => String, g: String => String): Thy_Header =
    8.30 +    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
    8.31  }
    8.32  
     9.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 16 09:31:23 2011 -0700
     9.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 16 15:02:20 2011 -0700
     9.3 @@ -9,7 +9,6 @@
     9.4  sig
     9.5    datatype action = Update | Remove
     9.6    val add_hook: (action -> string -> unit) -> unit
     9.7 -  val base_name: string -> string
     9.8    val get_names: unit -> string list
     9.9    val status: unit -> unit
    9.10    val lookup_theory: string -> theory option
    11.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 09:31:23 2011 -0700
    11.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 15:02:20 2011 -0700
    11.3 @@ -190,9 +190,7 @@
    11.4    {
    11.5      val master_dir = buffer.getDirectory
    11.6      val path = buffer.getSymlinkPath
    11.7 -    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
    11.8 -      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
    11.9 -    else (master_dir, path)
   11.10 +    (master_dir, path)
   11.11    }
   11.12  
   11.13  
   11.14 @@ -210,8 +208,8 @@
   11.15            case None =>
   11.16              val (master_dir, path) = buffer_path(buffer)
   11.17              Thy_Header.thy_name(path) match {
   11.18 -              case Some((prefix, name)) =>
   11.19 -                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
   11.20 +              case Some(name) =>
   11.21 +                Some(Document_Model.init(session, buffer, master_dir, path, name))
   11.22                case None => None
   11.23              }
   11.24          }
   11.25 @@ -334,8 +332,8 @@
   11.26        else {
   11.27          val vfs = VFSManager.getVFSForPath(master_dir)
   11.28          if (vfs.isInstanceOf[FileVFS])
   11.29 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path))
   11.30 -          // FIXME MiscUtilities.resolveSymlinks (!?)
   11.31 +          MiscUtilities.resolveSymlinks(
   11.32 +            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   11.33          else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   11.34        }
   11.35      }