1.1 --- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 08:21:52 2010 -0800
1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 08:41:16 2010 -0800
1.3 @@ -253,11 +253,12 @@
1.4
1.5 \begin{matharray}{rcl}
1.6 @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.7 + @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.8 @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.9 \end{matharray}
1.10
1.11 \begin{rail}
1.12 - 'declaration' ('(pervasive)')? target? text
1.13 + ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
1.14 ;
1.15 'declare' target? (thmrefs + 'and')
1.16 ;
1.17 @@ -275,6 +276,10 @@
1.18 declaration is applied to all possible contexts involved, including
1.19 the global background theory.
1.20
1.21 + \item @{command "syntax_declaration"} is similar to @{command
1.22 + "declaration"}, but is meant to affect only ``syntactic'' tools by
1.23 + convention (such as notation and type-checking information).
1.24 +
1.25 \item @{command "declare"}~@{text thms} declares theorems to the
1.26 current local theory context. No theorem binding is involved here,
1.27 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 28 08:21:52 2010 -0800
2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Nov 28 08:41:16 2010 -0800
2.3 @@ -273,11 +273,12 @@
2.4
2.5 \begin{matharray}{rcl}
2.6 \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}}} \\
2.7 + \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}}} \\
2.8 \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}}} \\
2.9 \end{matharray}
2.10
2.11 \begin{rail}
2.12 - 'declaration' ('(pervasive)')? target? text
2.13 + ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
2.14 ;
2.15 'declare' target? (thmrefs + 'and')
2.16 ;
2.17 @@ -295,6 +296,9 @@
2.18 declaration is applied to all possible contexts involved, including
2.19 the global background theory.
2.20
2.21 + \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
2.22 + convention (such as notation and type-checking information).
2.23 +
2.24 \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
2.25 current local theory context. No theorem binding is involved here,
2.26 unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
3.1 --- a/etc/isar-keywords-ZF.el Sun Nov 28 08:21:52 2010 -0800
3.2 +++ b/etc/isar-keywords-ZF.el Sun Nov 28 08:41:16 2010 -0800
3.3 @@ -172,6 +172,7 @@
3.4 "subsubsect"
3.5 "subsubsection"
3.6 "syntax"
3.7 + "syntax_declaration"
3.8 "term"
3.9 "text"
3.10 "text_raw"
3.11 @@ -395,6 +396,7 @@
3.12 "setup"
3.13 "simproc_setup"
3.14 "syntax"
3.15 + "syntax_declaration"
3.16 "text"
3.17 "text_raw"
3.18 "theorems"
4.1 --- a/etc/isar-keywords.el Sun Nov 28 08:21:52 2010 -0800
4.2 +++ b/etc/isar-keywords.el Sun Nov 28 08:41:16 2010 -0800
4.3 @@ -230,6 +230,7 @@
4.4 "subsubsect"
4.5 "subsubsection"
4.6 "syntax"
4.7 + "syntax_declaration"
4.8 "term"
4.9 "termination"
4.10 "text"
4.11 @@ -508,6 +509,7 @@
4.12 "sledgehammer_params"
4.13 "statespace"
4.14 "syntax"
4.15 + "syntax_declaration"
4.16 "text"
4.17 "text_raw"
4.18 "theorems"
5.1 --- a/src/Pure/Concurrent/bash.ML Sun Nov 28 08:21:52 2010 -0800
5.2 +++ b/src/Pure/Concurrent/bash.ML Sun Nov 28 08:41:16 2010 -0800
5.3 @@ -36,7 +36,8 @@
5.4 | Posix.Process.W_STOPPED s =>
5.5 Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
5.6 in Synchronized.change result (K res) end
5.7 - handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
5.8 + handle exn =>
5.9 + (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
5.10
5.11 fun terminate () =
5.12 let
6.1 --- a/src/Pure/General/file.ML Sun Nov 28 08:21:52 2010 -0800
6.2 +++ b/src/Pure/General/file.ML Sun Nov 28 08:41:16 2010 -0800
6.3 @@ -16,6 +16,7 @@
6.4 val exists: Path.T -> bool
6.5 val check: Path.T -> unit
6.6 val rm: Path.T -> unit
6.7 + val is_dir: Path.T -> bool
6.8 val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
6.9 val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
6.10 val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
6.11 @@ -71,6 +72,9 @@
6.12
6.13 val rm = OS.FileSys.remove o platform_path;
6.14
6.15 +fun is_dir path =
6.16 + the_default false (try OS.FileSys.isDir (platform_path path));
6.17 +
6.18
6.19 (* open files *)
6.20
6.21 @@ -128,9 +132,6 @@
6.22 SOME ids => is_equal (OS.FileSys.compare ids)
6.23 | NONE => false);
6.24
6.25 -fun is_dir path =
6.26 - the_default false (try OS.FileSys.isDir (platform_path path));
6.27 -
6.28 fun copy src dst =
6.29 if eq (src, dst) then ()
6.30 else
7.1 --- a/src/Pure/Isar/generic_target.ML Sun Nov 28 08:21:52 2010 -0800
7.2 +++ b/src/Pure/Isar/generic_target.ML Sun Nov 28 08:41:16 2010 -0800
7.3 @@ -7,28 +7,25 @@
7.4
7.5 signature GENERIC_TARGET =
7.6 sig
7.7 - val define: (((binding * typ) * mixfix) * (binding * term)
7.8 - -> term list * term list -> local_theory -> (term * thm) * local_theory)
7.9 - -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
7.10 - -> (term * (string * thm)) * local_theory
7.11 - val notes: (string
7.12 - -> (Attrib.binding * (thm list * Args.src list) list) list
7.13 - -> (Attrib.binding * (thm list * Args.src list) list) list
7.14 - -> local_theory -> local_theory)
7.15 - -> string -> (Attrib.binding * (thm list * Args.src list) list) list
7.16 - -> local_theory -> (string * thm list) list * local_theory
7.17 - val abbrev: (string * bool -> binding * mixfix -> term * term
7.18 - -> term list -> local_theory -> local_theory)
7.19 - -> string * bool -> (binding * mixfix) * term -> local_theory
7.20 - -> (term * term) * local_theory
7.21 + val define: (((binding * typ) * mixfix) * (binding * term) ->
7.22 + term list * term list -> local_theory -> (term * thm) * local_theory) ->
7.23 + (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
7.24 + (term * (string * thm)) * local_theory
7.25 + val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
7.26 + (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
7.27 + string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
7.28 + (string * thm list) list * local_theory
7.29 + val abbrev: (string * bool -> binding * mixfix -> term * term ->
7.30 + term list -> local_theory -> local_theory) ->
7.31 + string * bool -> (binding * mixfix) * term -> local_theory ->
7.32 + (term * term) * local_theory
7.33
7.34 val theory_declaration: declaration -> local_theory -> local_theory
7.35 - val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
7.36 - -> term list * term list -> local_theory -> (term * thm) * local_theory
7.37 - val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
7.38 - -> local_theory -> local_theory
7.39 - val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
7.40 - -> local_theory -> local_theory
7.41 + val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
7.42 + term list * term list -> local_theory -> (term * thm) * local_theory
7.43 + val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
7.44 + local_theory -> local_theory
7.45 + val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
7.46 end;
7.47
7.48 structure Generic_Target: GENERIC_TARGET =
8.1 --- a/src/Pure/Isar/isar_cmd.ML Sun Nov 28 08:21:52 2010 -0800
8.2 +++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 28 08:41:16 2010 -0800
8.3 @@ -16,7 +16,8 @@
8.4 val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
8.5 val add_axioms: (Attrib.binding * string) list -> theory -> theory
8.6 val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
8.7 - val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
8.8 + val declaration: {syntax: bool, pervasive: bool} ->
8.9 + Symbol_Pos.text * Position.T -> local_theory -> local_theory
8.10 val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
8.11 local_theory -> local_theory
8.12 val hide_class: bool -> xstring list -> theory -> theory
8.13 @@ -180,11 +181,13 @@
8.14
8.15 (* declarations *)
8.16
8.17 -fun declaration pervasive (txt, pos) =
8.18 +fun declaration {syntax, pervasive} (txt, pos) =
8.19 ML_Lex.read pos txt
8.20 |> ML_Context.expression pos
8.21 "val declaration: Morphism.declaration"
8.22 - ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
8.23 + ("Context.map_proof (Local_Theory." ^
8.24 + (if syntax then "syntax_declaration" else "declaration") ^ " " ^
8.25 + Bool.toString pervasive ^ " declaration)")
8.26 |> Context.proof_map;
8.27
8.28
9.1 --- a/src/Pure/Isar/isar_syn.ML Sun Nov 28 08:21:52 2010 -0800
9.2 +++ b/src/Pure/Isar/isar_syn.ML Sun Nov 28 08:41:16 2010 -0800
9.3 @@ -325,8 +325,16 @@
9.4 >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
9.5
9.6 val _ =
9.7 - Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
9.8 - (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
9.9 + Outer_Syntax.local_theory "declaration" "generic ML declaration"
9.10 + (Keyword.tag_ml Keyword.thy_decl)
9.11 + (Parse.opt_keyword "pervasive" -- Parse.ML_source
9.12 + >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
9.13 +
9.14 +val _ =
9.15 + Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
9.16 + (Keyword.tag_ml Keyword.thy_decl)
9.17 + (Parse.opt_keyword "pervasive" -- Parse.ML_source
9.18 + >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
9.19
9.20 val _ =
9.21 Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
10.1 --- a/src/Pure/Isar/locale.ML Sun Nov 28 08:21:52 2010 -0800
10.2 +++ b/src/Pure/Isar/locale.ML Sun Nov 28 08:41:16 2010 -0800
10.3 @@ -79,7 +79,7 @@
10.4 val print_locale: theory -> bool -> xstring -> unit
10.5 val print_registrations: Proof.context -> string -> unit
10.6 val locale_deps: theory ->
10.7 - { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
10.8 + {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
10.9 * term list list Symtab.table Symtab.table
10.10 end;
10.11
10.12 @@ -191,10 +191,9 @@
10.13 val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
10.14 val ts = instance_of thy name morph;
10.15 in
10.16 - case qs of
10.17 - [] => prt_inst ts
10.18 - | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
10.19 - Pretty.brk 1, prt_inst ts]
10.20 + (case qs of
10.21 + [] => prt_inst ts
10.22 + | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
10.23 end;
10.24
10.25
10.26 @@ -206,9 +205,9 @@
10.27
10.28 (* total order *)
10.29 fun ident_ord ((n: string, ts), (m, ss)) =
10.30 - case fast_string_ord (m, n) of
10.31 - EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
10.32 - | ord => ord;
10.33 + (case fast_string_ord (m, n) of
10.34 + EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
10.35 + | ord => ord);
10.36
10.37 local
10.38
10.39 @@ -256,7 +255,8 @@
10.40 then (deps, marked)
10.41 else
10.42 let
10.43 - val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
10.44 + val dependencies' =
10.45 + map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
10.46 val marked' = (name, instance) :: marked;
10.47 val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
10.48 in
10.49 @@ -309,9 +309,10 @@
10.50 val (_, s1) = Idtab.lookup reg1 id |> the;
10.51 val (morph2, s2) = Idtab.lookup reg2 id |> the;
10.52 val reg2' = Idtab.update (id, (morph2, s1)) reg2;
10.53 - val mix2' = case Inttab.lookup mix2 s2 of
10.54 - NONE => mix2 |
10.55 - SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
10.56 + val mix2' =
10.57 + (case Inttab.lookup mix2 s2 of
10.58 + NONE => mix2
10.59 + | SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs));
10.60 val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
10.61 (* FIXME print interpretations,
10.62 which is not straightforward without theory context *)
10.63 @@ -335,9 +336,9 @@
10.64 val thy = Context.theory_of context;
10.65 val (regs, mixins) = Registrations.get context;
10.66 in
10.67 - case Idtab.lookup regs (name, instance_of thy name morph) of
10.68 + (case Idtab.lookup regs (name, instance_of thy name morph) of
10.69 NONE => []
10.70 - | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
10.71 + | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial))
10.72 end;
10.73
10.74 fun compose_mixins mixins =
10.75 @@ -385,9 +386,12 @@
10.76 val {notes, ...} = the_locale thy name;
10.77 fun activate ((kind, facts), _) input =
10.78 let
10.79 - val mixin = case export' of NONE => Morphism.identity
10.80 - | SOME export => collect_mixins context (name, morph $> export) $> export;
10.81 - val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin))
10.82 + val mixin =
10.83 + (case export' of
10.84 + NONE => Morphism.identity
10.85 + | SOME export => collect_mixins context (name, morph $> export) $> export);
10.86 + val facts' = facts
10.87 + |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
10.88 in activ_elem (Notes (kind, facts')) input end;
10.89 in
10.90 fold_rev activate notes input
10.91 @@ -401,9 +405,8 @@
10.92 activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
10.93 (* FIXME type parameters *)
10.94 (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
10.95 - (if not (null defs)
10.96 - then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
10.97 - else I);
10.98 + (not (null defs) ?
10.99 + activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
10.100 val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
10.101 in
10.102 roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
10.103 @@ -443,12 +446,13 @@
10.104 val regs = Registrations.get context |> fst;
10.105 val base = instance_of thy name (morph $> export);
10.106 in
10.107 - case Idtab.lookup regs (name, base) of
10.108 - NONE => error ("No interpretation of locale " ^
10.109 + (case Idtab.lookup regs (name, base) of
10.110 + NONE =>
10.111 + error ("No interpretation of locale " ^
10.112 quote (extern thy name) ^ " and\nparameter instantiation " ^
10.113 space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
10.114 " available")
10.115 - | SOME (_, serial') => add_mixin serial' mixin context
10.116 + | SOME (_, serial') => add_mixin serial' mixin context)
10.117 end;
10.118
10.119 (* Note that a registration that would be subsumed by an existing one will not be
10.120 @@ -457,8 +461,7 @@
10.121 fun add_registration (name, base_morph) mixin export context =
10.122 let
10.123 val thy = Context.theory_of context;
10.124 - val mix = case mixin of NONE => Morphism.identity
10.125 - | SOME (mix, _) => mix;
10.126 + val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
10.127 val morph = base_morph $> mix;
10.128 val inst = instance_of thy name morph;
10.129 in
10.130 @@ -470,8 +473,10 @@
10.131 |> roundup thy (add_reg thy export) export (name, morph)
10.132 |> snd
10.133 (* add mixin *)
10.134 - |> (case mixin of NONE => I
10.135 - | SOME mixin => amend_registration (name, morph) mixin export)
10.136 + |>
10.137 + (case mixin of
10.138 + NONE => I
10.139 + | SOME mixin => amend_registration (name, morph) mixin export)
10.140 (* activate import hierarchy as far as not already active *)
10.141 |> activate_facts (SOME export) (name, morph)
10.142 end;
10.143 @@ -551,7 +556,7 @@
10.144 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
10.145
10.146
10.147 -(* Tactic *)
10.148 +(* Tactics *)
10.149
10.150 fun gen_intro_locales_tac intros_tac eager ctxt =
10.151 intros_tac
10.152 @@ -593,11 +598,10 @@
10.153 let
10.154 val thy = ProofContext.theory_of ctxt;
10.155 in
10.156 - (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
10.157 - [] => Pretty.str ("no interpretations")
10.158 - | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
10.159 - |> Pretty.writeln
10.160 - end;
10.161 + (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
10.162 + [] => Pretty.str ("no interpretations")
10.163 + | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
10.164 + end |> Pretty.writeln;
10.165
10.166 fun locale_deps thy =
10.167 let
10.168 @@ -605,16 +609,17 @@
10.169 fun add_locale_node name =
10.170 let
10.171 val params = params_of thy name;
10.172 - val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
10.173 - val registrations = map (instance_of thy name o snd)
10.174 - (registrations_of (Context.Theory thy) name);
10.175 - in
10.176 - Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
10.177 + val axioms =
10.178 + these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
10.179 + val registrations =
10.180 + map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
10.181 + in
10.182 + Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
10.183 end;
10.184 fun add_locale_deps name =
10.185 let
10.186 - val dependencies = (map o apsnd) (instance_of thy name o op $>)
10.187 - (dependencies_of thy name);
10.188 + val dependencies =
10.189 + (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name);
10.190 in
10.191 fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
10.192 deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
11.1 --- a/src/Pure/Isar/named_target.ML Sun Nov 28 08:21:52 2010 -0800
11.2 +++ b/src/Pure/Isar/named_target.ML Sun Nov 28 08:41:16 2010 -0800
11.3 @@ -38,7 +38,7 @@
11.4
11.5 (* generic declarations *)
11.6
11.7 -fun locale_declaration locale { syntax, pervasive } decl lthy =
11.8 +fun locale_declaration locale {syntax, pervasive} decl lthy =
11.9 let
11.10 val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
11.11 val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
11.12 @@ -48,9 +48,9 @@
11.13 |> Local_Theory.target (add locale locale_decl)
11.14 end;
11.15
11.16 -fun target_declaration (Target {target, ...}) { syntax, pervasive } =
11.17 +fun target_declaration (Target {target, ...}) {syntax, pervasive} =
11.18 if target = "" then Generic_Target.theory_declaration
11.19 - else locale_declaration target { syntax = syntax, pervasive = pervasive };
11.20 + else locale_declaration target {syntax = syntax, pervasive = pervasive};
11.21
11.22
11.23 (* consts in locales *)
11.24 @@ -81,7 +81,7 @@
11.25 end;
11.26
11.27 fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
11.28 - locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
11.29 + locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
11.30
11.31
11.32 (* define *)
11.33 @@ -106,7 +106,7 @@
11.34
11.35 (* notes *)
11.36
11.37 -fun locale_notes locale kind global_facts local_facts lthy =
11.38 +fun locale_notes locale kind global_facts local_facts lthy =
11.39 let
11.40 val global_facts' = Attrib.map_facts (K I) global_facts;
11.41 val local_facts' = Element.facts_map
11.42 @@ -119,7 +119,7 @@
11.43
11.44 fun target_notes (Target {target, is_locale, ...}) =
11.45 if is_locale then locale_notes target
11.46 - else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
11.47 + else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
11.48
11.49
11.50 (* abbrev *)
11.51 @@ -156,10 +156,11 @@
11.52 val elems =
11.53 (if null fixes then [] else [Element.Fixes fixes]) @
11.54 (if null assumes then [] else [Element.Assumes assumes]);
11.55 - val body_elems = if not is_locale then []
11.56 + val body_elems =
11.57 + if not is_locale then []
11.58 else if null elems then [Pretty.block target_name]
11.59 else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
11.60 - map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
11.61 + map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
11.62 in
11.63 Pretty.block [Pretty.command "theory", Pretty.brk 1,
11.64 Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
11.65 @@ -185,9 +186,9 @@
11.66 notes = Generic_Target.notes (target_notes ta),
11.67 abbrev = Generic_Target.abbrev (target_abbrev ta),
11.68 declaration = fn pervasive => target_declaration ta
11.69 - { syntax = false, pervasive = pervasive },
11.70 + {syntax = false, pervasive = pervasive},
11.71 syntax_declaration = fn pervasive => target_declaration ta
11.72 - { syntax = true, pervasive = pervasive },
11.73 + {syntax = true, pervasive = pervasive},
11.74 pretty = pretty ta,
11.75 exit = Local_Theory.target_of}
11.76 end;
12.1 --- a/src/Pure/Isar/overloading.ML Sun Nov 28 08:21:52 2010 -0800
12.2 +++ b/src/Pure/Isar/overloading.ML Sun Nov 28 08:41:16 2010 -0800
12.3 @@ -48,15 +48,16 @@
12.4 );
12.5
12.6 fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
12.7 - secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let
12.8 + secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
12.9 + let
12.10 val (((primary_constraints', secondary_constraints'),
12.11 (((improve', subst'), consider_abbrevs'), unchecks')), passed')
12.12 = f (((primary_constraints, secondary_constraints),
12.13 (((improve, subst), consider_abbrevs), unchecks)), passed)
12.14 in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
12.15 improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
12.16 - unchecks = unchecks', passed = passed'
12.17 - } end);
12.18 + unchecks = unchecks', passed = passed' }
12.19 + end);
12.20
12.21 val mark_passed = (map_improvable_syntax o apsnd) (K true);
12.22
12.23 @@ -80,7 +81,8 @@
12.24 | NONE => NONE)
12.25 | _ => NONE) t;
12.26 val ts'' = if is_abbrev then ts' else map apply_subst ts';
12.27 - in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
12.28 + in
12.29 + if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
12.30 if passed_or_abbrev then SOME (ts'', ctxt)
12.31 else SOME (ts'', ctxt
12.32 |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
12.33 @@ -166,9 +168,11 @@
12.34 fun conclude lthy =
12.35 let
12.36 val overloading = get_overloading lthy;
12.37 - val _ = if null overloading then () else
12.38 - error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
12.39 - o Syntax.string_of_term lthy o Const o fst) overloading));
12.40 + val _ =
12.41 + if null overloading then ()
12.42 + else
12.43 + error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
12.44 + o Syntax.string_of_term lthy o Const o fst) overloading));
12.45 in lthy end;
12.46
12.47 fun gen_overloading prep_const raw_overloading thy =
13.1 --- a/src/Pure/System/isabelle_system.ML Sun Nov 28 08:21:52 2010 -0800
13.2 +++ b/src/Pure/System/isabelle_system.ML Sun Nov 28 08:41:16 2010 -0800
13.3 @@ -41,7 +41,8 @@
13.4
13.5 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
13.6
13.7 -val mkdir = OS.FileSys.mkDir o File.platform_path;
13.8 +fun mkdir path =
13.9 + if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
13.10
13.11 fun copy_dir src dst =
13.12 if File.eq (src, dst) then ()