# HG changeset patch # User wenzelm # Date 1313529902 -7200 # Node ID 47e6986336f5ebc0c8421480d5019aad2d4422e6 # Parent 7e3a026f014f9ffee882a05359ea1608179e2f8d# Parent 1ea760da0f2d715242b09b441f5f2302965d1605 merged diff -r 7e3a026f014f -r 47e6986336f5 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Pure/General/position.ML Tue Aug 16 23:25:02 2011 +0200 @@ -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 7e3a026f014f -r 47e6986336f5 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Pure/PIDE/document.ML Tue Aug 16 23:25:02 2011 +0200 @@ -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 7e3a026f014f -r 47e6986336f5 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Pure/PIDE/document.scala Tue Aug 16 23:25:02 2011 +0200 @@ -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 7e3a026f014f -r 47e6986336f5 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Pure/System/session.scala Tue Aug 16 23:25:02 2011 +0200 @@ -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 7e3a026f014f -r 47e6986336f5 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Pure/Thy/thy_header.scala Tue Aug 16 23:25:02 2011 +0200 @@ -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 7e3a026f014f -r 47e6986336f5 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Pure/Thy/thy_info.ML Tue Aug 16 23:25:02 2011 +0200 @@ -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 7e3a026f014f -r 47e6986336f5 src/Pure/Thy/thy_info.scala diff -r 7e3a026f014f -r 47e6986336f5 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Aug 16 13:07:52 2011 -0700 +++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 16 23:25:02 2011 +0200 @@ -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)) } }