merged
authorwenzelm
Sun Nov 28 16:42:54 2010 +0100 (2010-11-28)
changeset 4078861ebeb050db1
parent 40787 d122dce6562d
parent 40785 c755df0f7062
child 40789 301e91df039d
child 40797 1b15d1805b72
merged
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 15:21:02 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     3.2 +++ b/etc/isar-keywords-ZF.el	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     4.2 +++ b/etc/isar-keywords.el	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     5.2 +++ b/src/Pure/Concurrent/bash.ML	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     6.2 +++ b/src/Pure/General/file.ML	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     7.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     8.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 28 16:42:54 2010 +0100
     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 15:21:02 2010 +0100
    10.2 +++ b/src/Pure/Isar/locale.ML	Sun Nov 28 16:42:54 2010 +0100
    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 15:21:02 2010 +0100
    11.2 +++ b/src/Pure/Isar/named_target.ML	Sun Nov 28 16:42:54 2010 +0100
    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 15:21:02 2010 +0100
    12.2 +++ b/src/Pure/Isar/overloading.ML	Sun Nov 28 16:42:54 2010 +0100
    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 15:21:02 2010 +0100
    13.2 +++ b/src/Pure/System/isabelle_system.ML	Sun Nov 28 16:42:54 2010 +0100
    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 ()