1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -12,21 +12,20 @@
     1.4    type outer_syntax
     1.5    val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
     1.6    val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
     1.7 -  val command: string -> string -> Keyword.T ->
     1.8 +  type command_spec = string * Keyword.T
     1.9 +  val command: command_spec -> string ->
    1.10      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.11 -  val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
    1.12 +  val markup_command: Thy_Output.markup -> command_spec -> string ->
    1.13      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.14 -  val improper_command: string -> string -> Keyword.T ->
    1.15 +  val improper_command: command_spec -> string ->
    1.16      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.17 -  val internal_command: string ->
    1.18 -    (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.19 -  val local_theory': string -> string -> Keyword.T ->
    1.20 +  val local_theory': command_spec -> string ->
    1.21      (bool -> local_theory -> local_theory) parser -> unit
    1.22 -  val local_theory: string -> string -> Keyword.T ->
    1.23 +  val local_theory: command_spec -> string ->
    1.24      (local_theory -> local_theory) parser -> unit
    1.25 -  val local_theory_to_proof': string -> string -> Keyword.T ->
    1.26 +  val local_theory_to_proof': command_spec -> string ->
    1.27      (bool -> local_theory -> Proof.state) parser -> unit
    1.28 -  val local_theory_to_proof: string -> string -> Keyword.T ->
    1.29 +  val local_theory_to_proof: command_spec -> string ->
    1.30      (local_theory -> Proof.state) parser -> unit
    1.31    val print_outer_syntax: unit -> unit
    1.32    val scan: Position.T -> string -> Token.T list
    1.33 @@ -117,21 +116,24 @@
    1.34  
    1.35  (** global outer syntax **)
    1.36  
    1.37 +type command_spec = string * Keyword.T;
    1.38 +
    1.39  local
    1.40  
    1.41  (*synchronized wrt. Keywords*)
    1.42  val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
    1.43  
    1.44 -fun add_command name kind cmd = CRITICAL (fn () =>
    1.45 +fun add_command (name, kind) cmd = CRITICAL (fn () =>
    1.46    let
    1.47      val thy = ML_Context.the_global_context ();
    1.48      val _ =
    1.49        (case try (Thy_Header.the_keyword thy) name of
    1.50 -        SOME k =>
    1.51 -          if k = SOME kind then ()
    1.52 +        SOME spec =>
    1.53 +          if Option.map Keyword.spec spec = SOME kind then ()
    1.54            else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
    1.55        | NONE =>
    1.56 -          if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
    1.57 +          if Context.theory_name thy = Context.PureN
    1.58 +          then Keyword.define (name, SOME kind)
    1.59            else error ("Undeclared outer syntax command " ^ quote name));
    1.60    in
    1.61      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    1.62 @@ -146,25 +148,22 @@
    1.63  
    1.64  fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
    1.65  
    1.66 -fun command name comment kind parse =
    1.67 -  add_command name kind (make_command comment NONE false parse);
    1.68 +fun command command_spec comment parse =
    1.69 +  add_command command_spec (make_command comment NONE false parse);
    1.70  
    1.71 -fun markup_command markup name comment kind parse =
    1.72 -  add_command name kind (make_command comment (SOME markup) false parse);
    1.73 +fun markup_command markup command_spec comment parse =
    1.74 +  add_command command_spec (make_command comment (SOME markup) false parse);
    1.75  
    1.76 -fun improper_command name comment kind parse =
    1.77 -  add_command name kind (make_command comment NONE true parse);
    1.78 -
    1.79 -fun internal_command name parse =
    1.80 -  command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
    1.81 +fun improper_command command_spec comment parse =
    1.82 +  add_command command_spec (make_command comment NONE true parse);
    1.83  
    1.84  end;
    1.85  
    1.86  
    1.87  (* local_theory commands *)
    1.88  
    1.89 -fun local_theory_command do_print trans name comment kind parse =
    1.90 -  command name comment kind (Parse.opt_target -- parse
    1.91 +fun local_theory_command do_print trans command_spec comment parse =
    1.92 +  command command_spec comment (Parse.opt_target -- parse
    1.93      >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
    1.94  
    1.95  val local_theory' = local_theory_command false Toplevel.local_theory';