--- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 08:21:52 2010 -0800
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 08:41:16 2010 -0800
@@ -253,11 +253,12 @@
\begin{matharray}{rcl}
@{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{rail}
- 'declaration' ('(pervasive)')? target? text
+ ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
;
'declare' target? (thmrefs + 'and')
;
@@ -275,6 +276,10 @@
declaration is applied to all possible contexts involved, including
the global background theory.
+ \item @{command "syntax_declaration"} is similar to @{command
+ "declaration"}, but is meant to affect only ``syntactic'' tools by
+ convention (such as notation and type-checking information).
+
\item @{command "declare"}~@{text thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike @{command "theorems"} or @{command "lemmas"} (cf.\
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 28 08:21:52 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 28 08:41:16 2010 -0800
@@ -273,11 +273,12 @@
\begin{matharray}{rcl}
\indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
\begin{rail}
- 'declaration' ('(pervasive)')? target? text
+ ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
;
'declare' target? (thmrefs + 'and')
;
@@ -295,6 +296,9 @@
declaration is applied to all possible contexts involved, including
the global background theory.
+ \item \hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}} is similar to \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}, but is meant to affect only ``syntactic'' tools by
+ convention (such as notation and type-checking information).
+
\item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
--- a/etc/isar-keywords-ZF.el Sun Nov 28 08:21:52 2010 -0800
+++ b/etc/isar-keywords-ZF.el Sun Nov 28 08:41:16 2010 -0800
@@ -172,6 +172,7 @@
"subsubsect"
"subsubsection"
"syntax"
+ "syntax_declaration"
"term"
"text"
"text_raw"
@@ -395,6 +396,7 @@
"setup"
"simproc_setup"
"syntax"
+ "syntax_declaration"
"text"
"text_raw"
"theorems"
--- a/etc/isar-keywords.el Sun Nov 28 08:21:52 2010 -0800
+++ b/etc/isar-keywords.el Sun Nov 28 08:41:16 2010 -0800
@@ -230,6 +230,7 @@
"subsubsect"
"subsubsection"
"syntax"
+ "syntax_declaration"
"term"
"termination"
"text"
@@ -508,6 +509,7 @@
"sledgehammer_params"
"statespace"
"syntax"
+ "syntax_declaration"
"text"
"text_raw"
"theorems"
--- a/src/Pure/Concurrent/bash.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Concurrent/bash.ML Sun Nov 28 08:41:16 2010 -0800
@@ -36,7 +36,8 @@
| Posix.Process.W_STOPPED s =>
Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
in Synchronized.change result (K res) end
- handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
+ handle exn =>
+ (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
fun terminate () =
let
--- a/src/Pure/General/file.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/General/file.ML Sun Nov 28 08:41:16 2010 -0800
@@ -16,6 +16,7 @@
val exists: Path.T -> bool
val check: Path.T -> unit
val rm: Path.T -> unit
+ val is_dir: Path.T -> bool
val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -71,6 +72,9 @@
val rm = OS.FileSys.remove o platform_path;
+fun is_dir path =
+ the_default false (try OS.FileSys.isDir (platform_path path));
+
(* open files *)
@@ -128,9 +132,6 @@
SOME ids => is_equal (OS.FileSys.compare ids)
| NONE => false);
-fun is_dir path =
- the_default false (try OS.FileSys.isDir (platform_path path));
-
fun copy src dst =
if eq (src, dst) then ()
else
--- a/src/Pure/Isar/generic_target.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Isar/generic_target.ML Sun Nov 28 08:41:16 2010 -0800
@@ -7,28 +7,25 @@
signature GENERIC_TARGET =
sig
- val define: (((binding * typ) * mixfix) * (binding * term)
- -> term list * term list -> local_theory -> (term * thm) * local_theory)
- -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
- -> (term * (string * thm)) * local_theory
- val notes: (string
- -> (Attrib.binding * (thm list * Args.src list) list) list
- -> (Attrib.binding * (thm list * Args.src list) list) list
- -> local_theory -> local_theory)
- -> string -> (Attrib.binding * (thm list * Args.src list) list) list
- -> local_theory -> (string * thm list) list * local_theory
- val abbrev: (string * bool -> binding * mixfix -> term * term
- -> term list -> local_theory -> local_theory)
- -> string * bool -> (binding * mixfix) * term -> local_theory
- -> (term * term) * local_theory
+ val define: (((binding * typ) * mixfix) * (binding * term) ->
+ term list * term list -> local_theory -> (term * thm) * local_theory) ->
+ (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ (term * (string * thm)) * local_theory
+ val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+ (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
+ string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
+ (string * thm list) list * local_theory
+ val abbrev: (string * bool -> binding * mixfix -> term * term ->
+ term list -> local_theory -> local_theory) ->
+ string * bool -> (binding * mixfix) * term -> local_theory ->
+ (term * term) * local_theory
val theory_declaration: declaration -> local_theory -> local_theory
- val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
- -> term list * term list -> local_theory -> (term * thm) * local_theory
- val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
- -> local_theory -> local_theory
- val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
- -> local_theory -> local_theory
+ val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+ term list * term list -> local_theory -> (term * thm) * local_theory
+ val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+ local_theory -> local_theory
+ val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
end;
structure Generic_Target: GENERIC_TARGET =
--- a/src/Pure/Isar/isar_cmd.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 28 08:41:16 2010 -0800
@@ -16,7 +16,8 @@
val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
val add_axioms: (Attrib.binding * string) list -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
- val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
+ val declaration: {syntax: bool, pervasive: bool} ->
+ Symbol_Pos.text * Position.T -> local_theory -> local_theory
val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
local_theory -> local_theory
val hide_class: bool -> xstring list -> theory -> theory
@@ -180,11 +181,13 @@
(* declarations *)
-fun declaration pervasive (txt, pos) =
+fun declaration {syntax, pervasive} (txt, pos) =
ML_Lex.read pos txt
|> ML_Context.expression pos
"val declaration: Morphism.declaration"
- ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
+ ("Context.map_proof (Local_Theory." ^
+ (if syntax then "syntax_declaration" else "declaration") ^ " " ^
+ Bool.toString pervasive ^ " declaration)")
|> Context.proof_map;
--- a/src/Pure/Isar/isar_syn.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Isar/isar_syn.ML Sun Nov 28 08:41:16 2010 -0800
@@ -325,8 +325,16 @@
>> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
val _ =
- Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
- (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
+ Outer_Syntax.local_theory "declaration" "generic ML declaration"
+ (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.opt_keyword "pervasive" -- Parse.ML_source
+ >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
+
+val _ =
+ Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
+ (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.opt_keyword "pervasive" -- Parse.ML_source
+ >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
val _ =
Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
--- a/src/Pure/Isar/locale.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Isar/locale.ML Sun Nov 28 08:41:16 2010 -0800
@@ -79,7 +79,7 @@
val print_locale: theory -> bool -> xstring -> unit
val print_registrations: Proof.context -> string -> unit
val locale_deps: theory ->
- { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
+ {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
* term list list Symtab.table Symtab.table
end;
@@ -191,10 +191,9 @@
val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
val ts = instance_of thy name morph;
in
- case qs of
- [] => prt_inst ts
- | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
- Pretty.brk 1, prt_inst ts]
+ (case qs of
+ [] => prt_inst ts
+ | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
end;
@@ -206,9 +205,9 @@
(* total order *)
fun ident_ord ((n: string, ts), (m, ss)) =
- case fast_string_ord (m, n) of
- EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
- | ord => ord;
+ (case fast_string_ord (m, n) of
+ EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
+ | ord => ord);
local
@@ -256,7 +255,8 @@
then (deps, marked)
else
let
- val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
+ val dependencies' =
+ map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
val marked' = (name, instance) :: marked;
val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
in
@@ -309,9 +309,10 @@
val (_, s1) = Idtab.lookup reg1 id |> the;
val (morph2, s2) = Idtab.lookup reg2 id |> the;
val reg2' = Idtab.update (id, (morph2, s1)) reg2;
- val mix2' = case Inttab.lookup mix2 s2 of
- NONE => mix2 |
- SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
+ val mix2' =
+ (case Inttab.lookup mix2 s2 of
+ NONE => mix2
+ | SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs));
val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
(* FIXME print interpretations,
which is not straightforward without theory context *)
@@ -335,9 +336,9 @@
val thy = Context.theory_of context;
val (regs, mixins) = Registrations.get context;
in
- case Idtab.lookup regs (name, instance_of thy name morph) of
+ (case Idtab.lookup regs (name, instance_of thy name morph) of
NONE => []
- | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
+ | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial))
end;
fun compose_mixins mixins =
@@ -385,9 +386,12 @@
val {notes, ...} = the_locale thy name;
fun activate ((kind, facts), _) input =
let
- val mixin = case export' of NONE => Morphism.identity
- | SOME export => collect_mixins context (name, morph $> export) $> export;
- val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin))
+ val mixin =
+ (case export' of
+ NONE => Morphism.identity
+ | SOME export => collect_mixins context (name, morph $> export) $> export);
+ val facts' = facts
+ |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
in activ_elem (Notes (kind, facts')) input end;
in
fold_rev activate notes input
@@ -401,9 +405,8 @@
activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
(* FIXME type parameters *)
(case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
- (if not (null defs)
- then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
- else I);
+ (not (null defs) ?
+ activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
in
roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
@@ -443,12 +446,13 @@
val regs = Registrations.get context |> fst;
val base = instance_of thy name (morph $> export);
in
- case Idtab.lookup regs (name, base) of
- NONE => error ("No interpretation of locale " ^
+ (case Idtab.lookup regs (name, base) of
+ NONE =>
+ error ("No interpretation of locale " ^
quote (extern thy name) ^ " and\nparameter instantiation " ^
space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
" available")
- | SOME (_, serial') => add_mixin serial' mixin context
+ | SOME (_, serial') => add_mixin serial' mixin context)
end;
(* Note that a registration that would be subsumed by an existing one will not be
@@ -457,8 +461,7 @@
fun add_registration (name, base_morph) mixin export context =
let
val thy = Context.theory_of context;
- val mix = case mixin of NONE => Morphism.identity
- | SOME (mix, _) => mix;
+ val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
val morph = base_morph $> mix;
val inst = instance_of thy name morph;
in
@@ -470,8 +473,10 @@
|> roundup thy (add_reg thy export) export (name, morph)
|> snd
(* add mixin *)
- |> (case mixin of NONE => I
- | SOME mixin => amend_registration (name, morph) mixin export)
+ |>
+ (case mixin of
+ NONE => I
+ | SOME mixin => amend_registration (name, morph) mixin export)
(* activate import hierarchy as far as not already active *)
|> activate_facts (SOME export) (name, morph)
end;
@@ -551,7 +556,7 @@
Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
-(* Tactic *)
+(* Tactics *)
fun gen_intro_locales_tac intros_tac eager ctxt =
intros_tac
@@ -593,11 +598,10 @@
let
val thy = ProofContext.theory_of ctxt;
in
- (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
- [] => Pretty.str ("no interpretations")
- | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
- |> Pretty.writeln
- end;
+ (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
+ [] => Pretty.str ("no interpretations")
+ | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+ end |> Pretty.writeln;
fun locale_deps thy =
let
@@ -605,16 +609,17 @@
fun add_locale_node name =
let
val params = params_of thy name;
- val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
- val registrations = map (instance_of thy name o snd)
- (registrations_of (Context.Theory thy) name);
- in
- Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
+ val axioms =
+ these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
+ val registrations =
+ map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
+ in
+ Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
end;
fun add_locale_deps name =
let
- val dependencies = (map o apsnd) (instance_of thy name o op $>)
- (dependencies_of thy name);
+ val dependencies =
+ (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name);
in
fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
--- a/src/Pure/Isar/named_target.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Isar/named_target.ML Sun Nov 28 08:41:16 2010 -0800
@@ -38,7 +38,7 @@
(* generic declarations *)
-fun locale_declaration locale { syntax, pervasive } decl lthy =
+fun locale_declaration locale {syntax, pervasive} decl lthy =
let
val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
@@ -48,9 +48,9 @@
|> Local_Theory.target (add locale locale_decl)
end;
-fun target_declaration (Target {target, ...}) { syntax, pervasive } =
+fun target_declaration (Target {target, ...}) {syntax, pervasive} =
if target = "" then Generic_Target.theory_declaration
- else locale_declaration target { syntax = syntax, pervasive = pervasive };
+ else locale_declaration target {syntax = syntax, pervasive = pervasive};
(* consts in locales *)
@@ -81,7 +81,7 @@
end;
fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
- locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
+ locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
(* define *)
@@ -106,7 +106,7 @@
(* notes *)
-fun locale_notes locale kind global_facts local_facts lthy =
+fun locale_notes locale kind global_facts local_facts lthy =
let
val global_facts' = Attrib.map_facts (K I) global_facts;
val local_facts' = Element.facts_map
@@ -119,7 +119,7 @@
fun target_notes (Target {target, is_locale, ...}) =
if is_locale then locale_notes target
- else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+ else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
(* abbrev *)
@@ -156,10 +156,11 @@
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
(if null assumes then [] else [Element.Assumes assumes]);
- val body_elems = if not is_locale then []
+ val body_elems =
+ if not is_locale then []
else if null elems then [Pretty.block target_name]
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
- map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
+ map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
in
Pretty.block [Pretty.command "theory", Pretty.brk 1,
Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
@@ -185,9 +186,9 @@
notes = Generic_Target.notes (target_notes ta),
abbrev = Generic_Target.abbrev (target_abbrev ta),
declaration = fn pervasive => target_declaration ta
- { syntax = false, pervasive = pervasive },
+ {syntax = false, pervasive = pervasive},
syntax_declaration = fn pervasive => target_declaration ta
- { syntax = true, pervasive = pervasive },
+ {syntax = true, pervasive = pervasive},
pretty = pretty ta,
exit = Local_Theory.target_of}
end;
--- a/src/Pure/Isar/overloading.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/Isar/overloading.ML Sun Nov 28 08:41:16 2010 -0800
@@ -48,15 +48,16 @@
);
fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
- secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let
+ secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
+ let
val (((primary_constraints', secondary_constraints'),
(((improve', subst'), consider_abbrevs'), unchecks')), passed')
= f (((primary_constraints, secondary_constraints),
(((improve, subst), consider_abbrevs), unchecks)), passed)
in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
- unchecks = unchecks', passed = passed'
- } end);
+ unchecks = unchecks', passed = passed' }
+ end);
val mark_passed = (map_improvable_syntax o apsnd) (K true);
@@ -80,7 +81,8 @@
| NONE => NONE)
| _ => NONE) t;
val ts'' = if is_abbrev then ts' else map apply_subst ts';
- in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
+ in
+ if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
if passed_or_abbrev then SOME (ts'', ctxt)
else SOME (ts'', ctxt
|> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
@@ -166,9 +168,11 @@
fun conclude lthy =
let
val overloading = get_overloading lthy;
- val _ = if null overloading then () else
- error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
- o Syntax.string_of_term lthy o Const o fst) overloading));
+ val _ =
+ if null overloading then ()
+ else
+ error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
+ o Syntax.string_of_term lthy o Const o fst) overloading));
in lthy end;
fun gen_overloading prep_const raw_overloading thy =
--- a/src/Pure/System/isabelle_system.ML Sun Nov 28 08:21:52 2010 -0800
+++ b/src/Pure/System/isabelle_system.ML Sun Nov 28 08:41:16 2010 -0800
@@ -41,7 +41,8 @@
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
-val mkdir = OS.FileSys.mkDir o File.platform_path;
+fun mkdir path =
+ if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
fun copy_dir src dst =
if File.eq (src, dst) then ()