Thy_Output.modes as proper option;
authorwenzelm
Thu May 16 21:09:58 2013 +0200 (2013-05-16)
changeset 52042aae07a3ff536
parent 52041 80e001b85332
child 52043 286629271d65
Thy_Output.modes as proper option;
etc/options
src/Pure/Thy/thy_output.ML
     1.1 --- a/etc/options	Thu May 16 20:50:01 2013 +0200
     1.2 +++ b/etc/options	Thu May 16 21:09:58 2013 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4    -- "indentation for pretty printing of display material"
     1.5  option thy_output_source : bool = false
     1.6    -- "print original source text rather than internal representation"
     1.7 -
     1.8 +option thy_output_modes : string = ""
     1.9 +  -- "additional print modes for document output (separated by commas)"
    1.10  
    1.11  option print_mode : string = ""
    1.12    -- "additional print modes for prover output (separated by commas)"
     2.1 --- a/src/Pure/Thy/thy_output.ML	Thu May 16 20:50:01 2013 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Thu May 16 21:09:58 2013 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4    val indent: int Config.T
     2.5    val source: bool Config.T
     2.6    val break: bool Config.T
     2.7 +  val modes: string Config.T
     2.8    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
     2.9    val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
    2.10    val intern_command: theory -> xstring -> string
    2.11 @@ -24,7 +25,6 @@
    2.12    val boolean: string -> bool
    2.13    val integer: string -> int
    2.14    datatype markup = Markup | MarkupEnv | Verbatim
    2.15 -  val modes: string list Unsynchronized.ref
    2.16    val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
    2.17    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    2.18    val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
    2.19 @@ -43,13 +43,14 @@
    2.20  structure Thy_Output: THY_OUTPUT =
    2.21  struct
    2.22  
    2.23 -(** global options **)
    2.24 +(** options **)
    2.25  
    2.26  val display = Attrib.setup_option_bool "thy_output_display";
    2.27  val break = Attrib.setup_option_bool "thy_output_break";
    2.28  val quotes = Attrib.setup_option_bool "thy_output_quotes";
    2.29  val indent = Attrib.setup_option_int "thy_output_indent";
    2.30  val source = Attrib.setup_option_bool "thy_output_source";
    2.31 +val modes = Attrib.setup_option_string "thy_output_modes";
    2.32  
    2.33  
    2.34  structure Wrappers = Proof_Data
    2.35 @@ -168,8 +169,6 @@
    2.36  
    2.37  (* eval_antiquote *)
    2.38  
    2.39 -val modes = Unsynchronized.ref ([]: string list);
    2.40 -
    2.41  fun eval_antiq lex state (ss, (pos, _)) =
    2.42    let
    2.43      val (opts, src) = Token.read_antiq lex antiq (ss, pos);
    2.44 @@ -177,7 +176,8 @@
    2.45      val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    2.46      val print_ctxt = Context_Position.set_visible false preview_ctxt;
    2.47      val _ = cmd preview_ctxt;
    2.48 -  in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end;
    2.49 +    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
    2.50 +  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    2.51  
    2.52  fun eval_antiquote lex state (txt, pos) =
    2.53    let