# HG changeset patch # User wenzelm # Date 1290958974 -3600 # Node ID 61ebeb050db11dffd4a7c4cfa31de92f4e18fb12 # Parent d122dce6562d969bbe8bfd1e10918a9234f131d2# Parent c755df0f7062515984b12753777002d7d18b4969 merged diff -r d122dce6562d -r 61ebeb050db1 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 15:21:02 2010 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 16:42:54 2010 +0100 @@ -253,11 +253,12 @@ \begin{matharray}{rcl} @{command_def "declaration"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "syntax_declaration"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "declare"} & : & @{text "local_theory \ 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.\ diff -r d122dce6562d -r 61ebeb050db1 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 28 15:21:02 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 28 16:42:54 2010 +0100 @@ -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.\ diff -r d122dce6562d -r 61ebeb050db1 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Sun Nov 28 15:21:02 2010 +0100 +++ b/etc/isar-keywords-ZF.el Sun Nov 28 16:42:54 2010 +0100 @@ -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" diff -r d122dce6562d -r 61ebeb050db1 etc/isar-keywords.el --- a/etc/isar-keywords.el Sun Nov 28 15:21:02 2010 +0100 +++ b/etc/isar-keywords.el Sun Nov 28 16:42:54 2010 +0100 @@ -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" diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Concurrent/bash.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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 diff -r d122dce6562d -r 61ebeb050db1 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/General/file.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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 diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Isar/generic_target.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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 = diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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; diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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) diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Isar/locale.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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)))) diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Isar/named_target.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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; diff -r d122dce6562d -r 61ebeb050db1 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/Isar/overloading.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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 = diff -r d122dce6562d -r 61ebeb050db1 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Sun Nov 28 15:21:02 2010 +0100 +++ b/src/Pure/System/isabelle_system.ML Sun Nov 28 16:42:54 2010 +0100 @@ -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 ()