69 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) |
69 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) |
70 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
70 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
71 in |
71 in |
72 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^ |
72 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^ |
73 (txt' |
73 (txt' |
74 |> (if ! Thy_Output.quotes then quote else I) |
74 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
75 |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
75 |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
76 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
76 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
77 end); |
77 end); |
78 |
78 |
79 in |
79 in |
80 |
80 |
91 |
91 |
92 val _ = Thy_Output.antiquotation "named_thms" |
92 val _ = Thy_Output.antiquotation "named_thms" |
93 (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) |
93 (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) |
94 (fn {context = ctxt, ...} => |
94 (fn {context = ctxt, ...} => |
95 map (apfst (Thy_Output.pretty_thm ctxt)) |
95 map (apfst (Thy_Output.pretty_thm ctxt)) |
96 #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I) |
96 #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I) |
97 #> (if ! Thy_Output.display |
97 #> (if Config.get ctxt Thy_Output.display |
98 then |
98 then |
99 map (fn (p, name) => |
99 map (fn (p, name) => |
100 Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^ |
100 Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ |
101 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}") |
101 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
102 #> space_implode "\\par\\smallskip%\n" |
102 #> space_implode "\\par\\smallskip%\n" |
103 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
103 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
104 else |
104 else |
105 map (fn (p, name) => |
105 map (fn (p, name) => |
106 Output.output (Pretty.str_of p) ^ |
106 Output.output (Pretty.str_of p) ^ |
107 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}") |
107 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
108 #> space_implode "\\par\\smallskip%\n" |
108 #> space_implode "\\par\\smallskip%\n" |
109 #> enclose "\\isa{" "}")); |
109 #> enclose "\\isa{" "}")); |
110 |
110 |
111 |
111 |
112 (* theory file *) |
112 (* theory file *) |
113 |
113 |
114 val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name) |
114 val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name) |
115 (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name])); |
115 (fn {context = ctxt, ...} => |
|
116 fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); |
116 |
117 |
117 |
118 |
118 (* Isabelle/Isar entities (with index) *) |
119 (* Isabelle/Isar entities (with index) *) |
119 |
120 |
120 local |
121 local |
150 in |
151 in |
151 if check ctxt name then |
152 if check ctxt name then |
152 idx ^ |
153 idx ^ |
153 (Output.output name |
154 (Output.output name |
154 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
155 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
155 |> (if ! Thy_Output.quotes then quote else I) |
156 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
156 |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
157 |> (if Config.get ctxt Thy_Output.display |
|
158 then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
157 else hyper o enclose "\\mbox{\\isa{" "}}")) |
159 else hyper o enclose "\\mbox{\\isa{" "}}")) |
158 else error ("Bad " ^ kind ^ " " ^ quote name) |
160 else error ("Bad " ^ kind ^ " " ^ quote name) |
159 end); |
161 end); |
160 |
162 |
161 fun entity_antiqs check markup kind = |
163 fun entity_antiqs check markup kind = |