doc-src/antiquote_setup.ML
changeset 38767 d8da44a8dd25
parent 37982 111ce9651564
child 39829 f5ea50decd9f
     1.1 --- a/doc-src/antiquote_setup.ML	Fri Aug 27 00:09:56 2010 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Fri Aug 27 12:40:20 2010 +0200
     1.3 @@ -71,8 +71,8 @@
     1.4      in
     1.5        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
     1.6        (txt'
     1.7 -      |> (if ! Thy_Output.quotes then quote else I)
     1.8 -      |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
     1.9 +      |> (if Config.get ctxt Thy_Output.quotes then quote else I)
    1.10 +      |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.11            else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.12      end);
    1.13  
    1.14 @@ -93,18 +93,18 @@
    1.15    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    1.16    (fn {context = ctxt, ...} =>
    1.17      map (apfst (Thy_Output.pretty_thm ctxt))
    1.18 -    #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
    1.19 -    #> (if ! Thy_Output.display
    1.20 +    #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
    1.21 +    #> (if Config.get ctxt Thy_Output.display
    1.22          then
    1.23            map (fn (p, name) =>
    1.24 -            Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
    1.25 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
    1.26 +            Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
    1.27 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.28            #> space_implode "\\par\\smallskip%\n"
    1.29            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.30          else
    1.31            map (fn (p, name) =>
    1.32              Output.output (Pretty.str_of p) ^
    1.33 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
    1.34 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.35            #> space_implode "\\par\\smallskip%\n"
    1.36            #> enclose "\\isa{" "}"));
    1.37  
    1.38 @@ -112,7 +112,8 @@
    1.39  (* theory file *)
    1.40  
    1.41  val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
    1.42 -  (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
    1.43 +  (fn {context = ctxt, ...} =>
    1.44 +    fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
    1.45  
    1.46  
    1.47  (* Isabelle/Isar entities (with index) *)
    1.48 @@ -152,8 +153,9 @@
    1.49            idx ^
    1.50            (Output.output name
    1.51              |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.52 -            |> (if ! Thy_Output.quotes then quote else I)
    1.53 -            |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.54 +            |> (if Config.get ctxt Thy_Output.quotes then quote else I)
    1.55 +            |> (if Config.get ctxt Thy_Output.display
    1.56 +                then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.57                  else hyper o enclose "\\mbox{\\isa{" "}}"))
    1.58          else error ("Bad " ^ kind ^ " " ^ quote name)
    1.59        end);