merged

--- a/Admin/Mercurial/cvsids	Tue Mar 10 22:22:52 2009 +0100
+++ b/Admin/Mercurial/cvsids	Tue Mar 10 22:50:19 2009 +0100
@@ -1,5 +1,6 @@
 Identifiers of some old CVS file versions
 =========================================
 
-src/Pure/type.ML    1.65        0d984ee030a1
+src/Pure/type.ML            1.65    0d984ee030a1
+src/Pure/General/file.ML    1.18    6cdd6a8da9b9
 

--- a/src/Pure/General/name_space.ML	Tue Mar 10 22:22:52 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 10 22:50:19 2009 +0100
@@ -33,6 +33,8 @@
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val add_path: string -> naming -> naming
+  val root_path: naming -> naming
+  val parent_path: naming -> naming
   val no_base_names: naming -> naming
   val qualified_names: naming -> naming
   val sticky_prefix: string -> naming -> naming
@@ -189,10 +191,13 @@
 val default_naming = make_naming ([], false, false);
 
 fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
-  if elems = "//" then ([], no_base_names, true)
-  else if elems = "/" then ([], no_base_names, qualified_names)
-  else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
-  else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+
+val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
+  ([], no_base_names, qualified_names));
+
+val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
+  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
 
 fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
   (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));

--- a/src/Pure/Isar/proof.ML	Tue Mar 10 22:22:52 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Mar 10 22:50:19 2009 +0100
@@ -677,18 +677,19 @@
 
 local
 
+fun qualified_binding a =
+  Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
+
 fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   let
     val atts = map (prep_att (theory_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
       ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
-    val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts));
+    val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   in
     state'
-    |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
     |> assume_i assumptions
     |> add_binds_i AutoBind.no_facts
-    |> map_context (ProofContext.restore_naming (context_of state))
     |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
   end;
 

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 10 22:22:52 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 10 22:50:19 2009 +0100
@@ -97,9 +97,8 @@
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
-  val no_base_names: Proof.context -> Proof.context
+  val sticky_prefix: string -> Proof.context -> Proof.context
   val qualified_names: Proof.context -> Proof.context
-  val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -263,9 +262,11 @@
 
 fun transfer_syntax thy =
   map_syntax (LocalSyntax.rebuild thy) #>
-  map_consts (fn (local_consts, _) =>
-    let val thy_consts = Sign.consts_of thy
-    in (Consts.merge (local_consts, thy_consts), thy_consts) end);
+  map_consts (fn consts as (local_consts, global_consts) =>
+    let val thy_consts = Sign.consts_of thy in
+      if Consts.eq_consts (thy_consts, global_consts) then consts
+      else (Consts.merge (local_consts, thy_consts), thy_consts)
+    end);
 
 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
 
@@ -945,9 +946,8 @@
 (* name space operations *)
 
 val add_path        = map_naming o NameSpace.add_path;
-val no_base_names   = map_naming NameSpace.no_base_names;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);
 

--- a/src/Pure/Isar/toplevel.ML	Tue Mar 10 22:22:52 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Mar 10 22:50:19 2009 +0100
@@ -293,7 +293,10 @@
 local
 
 fun debugging f x =
-  if ! debug then exception_trace (fn () => f x)
+  if ! debug then
+    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
+      SOME y => y
+    | NONE => raise UNDEF)
   else f x;
 
 fun toplevel_error f x =

--- a/src/Pure/consts.ML	Tue Mar 10 22:22:52 2009 +0100
+++ b/src/Pure/consts.ML	Tue Mar 10 22:50:19 2009 +0100
@@ -8,6 +8,7 @@
 signature CONSTS =
 sig
   type T
+  val eq_consts: T * T -> bool
   val abbrevs_of: T -> string list -> (term * term) list
   val dest: T ->
    {constants: (typ * term option) NameSpace.table,
@@ -53,6 +54,13 @@
   constraints: typ Symtab.table,
   rev_abbrevs: (term * term) list Symtab.table};
 
+fun eq_consts
+   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
+    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
+  pointer_eq (decls1, decls2) andalso
+  pointer_eq (constraints1, constraints2) andalso
+  pointer_eq (rev_abbrevs1, rev_abbrevs2);
+
 fun make_consts (decls, constraints, rev_abbrevs) =
   Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
 

--- a/src/Pure/sign.ML	Tue Mar 10 22:22:52 2009 +0100
+++ b/src/Pure/sign.ML	Tue Mar 10 22:50:19 2009 +0100
@@ -122,13 +122,13 @@
   val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   val del_trrules_i: ast Syntax.trrule list -> theory -> theory
   val add_path: string -> theory -> theory
+  val root_path: theory -> theory
   val parent_path: theory -> theory
-  val root_path: theory -> theory
+  val sticky_prefix: string -> theory -> theory
+  val no_base_names: theory -> theory
+  val qualified_names: theory -> theory
   val absolute_path: theory -> theory
   val local_path: theory -> theory
-  val no_base_names: theory -> theory
-  val qualified_names: theory -> theory
-  val sticky_prefix: string -> theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -619,17 +619,18 @@
 (* naming *)
 
 val add_path        = map_naming o NameSpace.add_path;
+val root_path       = map_naming NameSpace.root_path;
+val parent_path     = map_naming NameSpace.parent_path;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val no_base_names   = map_naming NameSpace.no_base_names;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
-val restore_naming  = map_naming o K o naming_of;
 
-val parent_path   = add_path "..";
-val root_path     = add_path "/";
-val absolute_path = add_path "//";
+val absolute_path = root_path o qualified_names;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val restore_naming  = map_naming o K o naming_of;
+
 
 (* hide names *)