1.1 --- a/doc-src/antiquote_setup.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
     1.6  
     1.7 -val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
     1.8 +val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
     1.9    (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
    1.10  
    1.11  
    1.12 @@ -56,7 +56,7 @@
    1.13  
    1.14  fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
    1.15  
    1.16 -fun index_ml name kind ml = ThyOutput.antiquotation name
    1.17 +fun index_ml name kind ml = Thy_Output.antiquotation name
    1.18    (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
    1.19    (fn {context = ctxt, ...} => fn (txt1, txt2) =>
    1.20      let
    1.21 @@ -71,8 +71,8 @@
    1.22      in
    1.23        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.24        (txt'
    1.25 -      |> (if ! ThyOutput.quotes then quote else I)
    1.26 -      |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.27 +      |> (if ! Thy_Output.quotes then quote else I)
    1.28 +      |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.29            else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.30      end);
    1.31  
    1.32 @@ -89,30 +89,30 @@
    1.33  
    1.34  (* named theorems *)
    1.35  
    1.36 -val _ = ThyOutput.antiquotation "named_thms"
    1.37 +val _ = Thy_Output.antiquotation "named_thms"
    1.38    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    1.39    (fn {context = ctxt, ...} =>
    1.40 -    map (apfst (ThyOutput.pretty_thm ctxt))
    1.41 -    #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
    1.42 -    #> (if ! ThyOutput.display
    1.43 +    map (apfst (Thy_Output.pretty_thm ctxt))
    1.44 +    #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
    1.45 +    #> (if ! Thy_Output.display
    1.46          then
    1.47            map (fn (p, name) =>
    1.48 -            Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
    1.49 -            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
    1.50 +            Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
    1.51 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
    1.52            #> space_implode "\\par\\smallskip%\n"
    1.53            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.54          else
    1.55            map (fn (p, name) =>
    1.56              Output.output (Pretty.str_of p) ^
    1.57 -            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
    1.58 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
    1.59            #> space_implode "\\par\\smallskip%\n"
    1.60            #> enclose "\\isa{" "}"));
    1.61  
    1.62  
    1.63  (* theory file *)
    1.64  
    1.65 -val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
    1.66 -  (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
    1.67 +val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
    1.68 +  (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
    1.69  
    1.70  
    1.71  (* Isabelle/Isar entities (with index) *)
    1.72 @@ -131,7 +131,7 @@
    1.73  val arg = enclose "{" "}" o clean_string;
    1.74  
    1.75  fun entity check markup kind index =
    1.76 -  ThyOutput.antiquotation
    1.77 +  Thy_Output.antiquotation
    1.78      (translate (fn " " => "_" | c => c) kind ^
    1.79        (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
    1.80      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.81 @@ -152,8 +152,8 @@
    1.82            idx ^
    1.83            (Output.output name
    1.84              |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.85 -            |> (if ! ThyOutput.quotes then quote else I)
    1.86 -            |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.87 +            |> (if ! Thy_Output.quotes then quote else I)
    1.88 +            |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.89                  else hyper o enclose "\\mbox{\\isa{" "}}"))
    1.90          else error ("Bad " ^ kind ^ " " ^ quote name)
    1.91        end);
    1.92 @@ -174,14 +174,14 @@
    1.93  val _ = entity_antiqs no_check "" "fact";
    1.94  val _ = entity_antiqs no_check "" "variable";
    1.95  val _ = entity_antiqs no_check "" "case";
    1.96 -val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
    1.97 -val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
    1.98 +val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
    1.99 +val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
   1.100  val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
   1.101  val _ = entity_antiqs no_check "" "inference";
   1.102  val _ = entity_antiqs no_check "isatt" "executable";
   1.103  val _ = entity_antiqs (K check_tool) "isatt" "tool";
   1.104  val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
   1.105 -val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
   1.106 +val _ = entity_antiqs (K Thy_Info.known_thy) "" "theory";
   1.107  
   1.108  end;
   1.109