src/Pure/Thy/thy_output.ML
changeset 32966 5b21661fe618
parent 32898 e871d897969c
child 33095 bbd52d2f8696
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 17 15:55:57 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 17 15:57:51 2009 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4            let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
     1.5              options opts (fn () => command src state) ();  (*preview errors!*)
     1.6              PrintMode.with_modes (! modes @ Latex.modes)
     1.7 -              (Output.no_warnings (options opts (fn () => command src state))) ()
     1.8 +              (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
     1.9            end
    1.10        | expand (Antiquote.Open _) = ""
    1.11        | expand (Antiquote.Close _) = "";
    1.12 @@ -416,22 +416,22 @@
    1.13  (* options *)
    1.14  
    1.15  val _ = add_options
    1.16 - [("show_types", Library.setmp Syntax.show_types o boolean),
    1.17 -  ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
    1.18 -  ("show_structs", Library.setmp show_structs o boolean),
    1.19 -  ("show_question_marks", Library.setmp show_question_marks o boolean),
    1.20 -  ("long_names", Library.setmp NameSpace.long_names o boolean),
    1.21 -  ("short_names", Library.setmp NameSpace.short_names o boolean),
    1.22 -  ("unique_names", Library.setmp NameSpace.unique_names o boolean),
    1.23 -  ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
    1.24 -  ("display", Library.setmp display o boolean),
    1.25 -  ("break", Library.setmp break o boolean),
    1.26 -  ("quotes", Library.setmp quotes o boolean),
    1.27 + [("show_types", setmp_CRITICAL Syntax.show_types o boolean),
    1.28 +  ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
    1.29 +  ("show_structs", setmp_CRITICAL show_structs o boolean),
    1.30 +  ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
    1.31 +  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
    1.32 +  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
    1.33 +  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
    1.34 +  ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
    1.35 +  ("display", setmp_CRITICAL display o boolean),
    1.36 +  ("break", setmp_CRITICAL break o boolean),
    1.37 +  ("quotes", setmp_CRITICAL quotes o boolean),
    1.38    ("mode", fn s => fn f => PrintMode.with_modes [s] f),
    1.39 -  ("margin", Pretty.setmp_margin o integer),
    1.40 -  ("indent", Library.setmp indent o integer),
    1.41 -  ("source", Library.setmp source o boolean),
    1.42 -  ("goals_limit", Library.setmp goals_limit o integer)];
    1.43 +  ("margin", Pretty.setmp_margin_CRITICAL o integer),
    1.44 +  ("indent", setmp_CRITICAL indent o integer),
    1.45 +  ("source", setmp_CRITICAL source o boolean),
    1.46 +  ("goals_limit", setmp_CRITICAL goals_limit o integer)];
    1.47  
    1.48  
    1.49  (* basic pretty printing *)