1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 27 00:02:32 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 27 00:09:56 2010 +0200
     1.3 @@ -11,15 +11,15 @@
     1.4    val indent: int Unsynchronized.ref
     1.5    val source: bool Unsynchronized.ref
     1.6    val break: bool Unsynchronized.ref
     1.7 -  val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
     1.8 -  val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
     1.9 +  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
    1.10 +  val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
    1.11    val defined_command: string -> bool
    1.12    val defined_option: string -> bool
    1.13    val print_antiquotations: unit -> unit
    1.14    val boolean: string -> bool
    1.15    val integer: string -> int
    1.16    val antiquotation: string -> 'a context_parser ->
    1.17 -    ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
    1.18 +    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit
    1.19    datatype markup = Markup | MarkupEnv | Verbatim
    1.20    val modes: string list Unsynchronized.ref
    1.21    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    1.22 @@ -45,28 +45,40 @@
    1.23  val break = Unsynchronized.ref false;
    1.24  
    1.25  
    1.26 +structure Wrappers = Proof_Data
    1.27 +(
    1.28 +  type T = ((unit -> string) -> unit -> string) list;
    1.29 +  fun init _ = [];
    1.30 +);
    1.31 +
    1.32 +fun add_wrapper wrapper = Wrappers.map (cons wrapper);
    1.33 +
    1.34 +val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
    1.35 +
    1.36 +
    1.37  
    1.38  (** maintain global antiquotations **)
    1.39  
    1.40  local
    1.41  
    1.42  val global_commands =
    1.43 -  Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
    1.44 +  Unsynchronized.ref
    1.45 +    (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table);
    1.46  
    1.47  val global_options =
    1.48 -  Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
    1.49 +  Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table);
    1.50  
    1.51 -fun add_item kind (name, x) tab =
    1.52 +fun add_item kind name item tab =
    1.53   (if not (Symtab.defined tab name) then ()
    1.54    else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name);
    1.55 -  Symtab.update (name, x) tab);
    1.56 +  Symtab.update (name, item) tab);
    1.57  
    1.58  in
    1.59  
    1.60 -fun add_commands xs =
    1.61 -  CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
    1.62 -fun add_options xs =
    1.63 -  CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
    1.64 +fun add_command name cmd =
    1.65 +  CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd));
    1.66 +fun add_option name opt =
    1.67 +  CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt));
    1.68  
    1.69  fun defined_command name = Symtab.defined (! global_commands) name;
    1.70  fun defined_option name = Symtab.defined (! global_options) name;
    1.71 @@ -77,18 +89,15 @@
    1.72        NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
    1.73      | SOME f =>
    1.74         (Position.report (Markup.doc_antiq name) pos;
    1.75 -        (fn state => f src state handle ERROR msg =>
    1.76 +        (fn state => fn ctxt => f src state ctxt handle ERROR msg =>
    1.77            cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    1.78              quote name ^ Position.str_of pos))))
    1.79    end;
    1.80  
    1.81 -fun option (name, s) f () =
    1.82 +fun option (name, s) ctxt =
    1.83    (case Symtab.lookup (! global_options) name of
    1.84      NONE => error ("Unknown document antiquotation option: " ^ quote name)
    1.85 -  | SOME opt => opt s f ());
    1.86 -
    1.87 -fun options [] f = f
    1.88 -  | options (opt :: opts) f = option opt (options opts f);
    1.89 +  | SOME opt => opt s ctxt);
    1.90  
    1.91  
    1.92  fun print_antiquotations () =
    1.93 @@ -100,10 +109,11 @@
    1.94  
    1.95  end;
    1.96  
    1.97 -fun antiquotation name scan out = add_commands [(name, fn src => fn state =>
    1.98 -  let val (x, ctxt) = Args.context_syntax "document antiquotation"
    1.99 -    scan src (Toplevel.presentation_context_of state)
   1.100 -  in out {source = src, state = state, context = ctxt} x end)];
   1.101 +fun antiquotation name scan out =
   1.102 +  add_command name
   1.103 +    (fn src => fn state => fn ctxt =>
   1.104 +      let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
   1.105 +      in out {source = src, state = state, context = ctxt'} x end);
   1.106  
   1.107  
   1.108  
   1.109 @@ -151,10 +161,13 @@
   1.110    let
   1.111      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
   1.112        | expand (Antiquote.Antiq (ss, (pos, _))) =
   1.113 -          let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
   1.114 -            options opts (fn () => command src state) ();  (*preview errors!*)
   1.115 -            Print_Mode.with_modes (! modes @ Latex.modes)
   1.116 -              (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
   1.117 +          let
   1.118 +            val (opts, src) = Token.read_antiq lex antiq (ss, pos);
   1.119 +            val opts_ctxt = fold option opts (Toplevel.presentation_context_of state);
   1.120 +            val cmd = wrap opts_ctxt (fn () => command src state opts_ctxt);
   1.121 +            val _ = cmd ();  (*preview errors!*)
   1.122 +          in
   1.123 +            Print_Mode.with_modes (! modes @ Latex.modes) (Output.no_warnings_CRITICAL cmd) ()
   1.124            end
   1.125        | expand (Antiquote.Open _) = ""
   1.126        | expand (Antiquote.Close _) = "";
   1.127 @@ -417,23 +430,22 @@
   1.128  
   1.129  (* options *)
   1.130  
   1.131 -val _ = add_options
   1.132 - [("show_types", setmp_CRITICAL Syntax.show_types o boolean),
   1.133 -  ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
   1.134 -  ("show_structs", setmp_CRITICAL show_structs o boolean),
   1.135 -  ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
   1.136 -  ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
   1.137 -  ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
   1.138 -  ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
   1.139 -  ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   1.140 -  ("display", setmp_CRITICAL display o boolean),
   1.141 -  ("break", setmp_CRITICAL break o boolean),
   1.142 -  ("quotes", setmp_CRITICAL quotes o boolean),
   1.143 -  ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
   1.144 -  ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   1.145 -  ("indent", setmp_CRITICAL indent o integer),
   1.146 -  ("source", setmp_CRITICAL source o boolean),
   1.147 -  ("goals_limit", setmp_CRITICAL goals_limit o integer)];
   1.148 +val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
   1.149 +val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
   1.150 +val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
   1.151 +val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks o boolean);
   1.152 +val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
   1.153 +val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
   1.154 +val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
   1.155 +val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
   1.156 +val _ = add_option "display" (add_wrapper o setmp_CRITICAL display o boolean);
   1.157 +val _ = add_option "break" (add_wrapper o setmp_CRITICAL break o boolean);
   1.158 +val _ = add_option "quotes" (add_wrapper o setmp_CRITICAL quotes o boolean);
   1.159 +val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
   1.160 +val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
   1.161 +val _ = add_option "indent" (add_wrapper o setmp_CRITICAL indent o integer);
   1.162 +val _ = add_option "source" (add_wrapper o setmp_CRITICAL source o boolean);
   1.163 +val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
   1.164  
   1.165  
   1.166  (* basic pretty printing *)