--- a/Admin/Mercurial/cvsids Wed Mar 11 08:45:47 2009 +0100
+++ b/Admin/Mercurial/cvsids Wed Mar 11 08:45:57 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/HOL/Docs/Main_Doc.thy Wed Mar 11 08:45:47 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy Wed Mar 11 08:45:57 2009 +0100
@@ -18,16 +18,16 @@
text{*
\begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisicated class structure is only hinted at.
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at.
\end{abstract}
\section{HOL}
-The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
+The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. (\textsc{ascii}: \verb$~$, \verb$&$, \verb$|$, \verb$-->$, \texttt{ALL}, \texttt{EX})
Overloaded operators:
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
@{text "0"} & @{typeof HOL.zero}\\
@{text "1"} & @{typeof HOL.one}\\
@{const HOL.plus} & @{typeof HOL.plus}\\
@@ -38,7 +38,7 @@
@{const HOL.divide} & @{typeof HOL.divide}\\
@{const HOL.abs} & @{typeof HOL.abs}\\
@{const HOL.sgn} & @{typeof HOL.sgn}\\
-@{const HOL.less_eq} & @{typeof HOL.less_eq}\\
+@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
@{const HOL.less} & @{typeof HOL.less}\\
@{const HOL.default} & @{typeof HOL.default}\\
@{const HOL.undefined} & @{typeof HOL.undefined}\\
@@ -109,13 +109,13 @@
Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"}
\bigskip
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
-@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} \qquad(\textsc{ascii} @{text":"})\\
-@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\
-@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\
+@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
+@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
+@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
@@ -129,7 +129,7 @@
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
@@ -137,9 +137,9 @@
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
@{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\
-@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
-@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
+@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
--- a/src/Pure/General/name_space.ML Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 11 08:45:57 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 Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 11 08:45:57 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 Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 11 08:45:57 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 Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Mar 11 08:45:57 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 Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/consts.ML Wed Mar 11 08:45:57 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 Wed Mar 11 08:45:47 2009 +0100
+++ b/src/Pure/sign.ML Wed Mar 11 08:45:57 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 *)