1.1 --- a/doc-src/antiquote_setup.ML Mon Mar 09 20:29:45 2009 +0100
1.2 +++ b/doc-src/antiquote_setup.ML Mon Mar 09 20:34:11 2009 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: Doc/antiquote_setup.ML
1.5 +(* Title: doc-src/antiquote_setup.ML
1.6 Author: Makarius
1.7
1.8 Auxiliary antiquotations for the Isabelle manuals.
1.9 @@ -52,87 +52,70 @@
1.10 fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
1.11 | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
1.12
1.13 -fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
1.14 +fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
1.15
1.16 -fun ml_functor _ = "val _ = ();"; (*no check!*)
1.17 +fun ml_functor _ = ""; (*no check!*)
1.18
1.19 -fun index_ml kind ml src ctxt (txt1, txt2) =
1.20 - let
1.21 - val txt = if txt2 = "" then txt1 else
1.22 - if kind = "type" then txt1 ^ " = " ^ txt2
1.23 - else if kind = "exception" then txt1 ^ " of " ^ txt2
1.24 - else txt1 ^ ": " ^ txt2;
1.25 - val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.26 - val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
1.27 - val kind' = if kind = "" then "ML" else "ML " ^ kind;
1.28 - in
1.29 - "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
1.30 - (txt'
1.31 - |> (if ! ThyOutput.quotes then quote else I)
1.32 - |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.33 - else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
1.34 - end;
1.35 -
1.36 -fun output_ml ctxt src =
1.37 - if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.38 - else
1.39 - split_lines
1.40 - #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
1.41 - #> space_implode "\\isasep\\isanewline%\n";
1.42 -
1.43 -fun ml_args x = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
1.44 +fun index_ml name kind ml = ThyOutput.antiquotation name
1.45 + (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
1.46 + (fn {context = ctxt, ...} => fn (txt1, txt2) =>
1.47 + let
1.48 + val txt =
1.49 + if txt2 = "" then txt1
1.50 + else if kind = "type" then txt1 ^ " = " ^ txt2
1.51 + else if kind = "exception" then txt1 ^ " of " ^ txt2
1.52 + else txt1 ^ ": " ^ txt2;
1.53 + val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.54 + val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
1.55 + val kind' = if kind = "" then "ML" else "ML " ^ kind;
1.56 + in
1.57 + "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
1.58 + (txt'
1.59 + |> (if ! ThyOutput.quotes then quote else I)
1.60 + |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.61 + else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
1.62 + end);
1.63
1.64 in
1.65
1.66 -val _ = ThyOutput.add_commands
1.67 - [("index_ML", ml_args (index_ml "" ml_val)),
1.68 - ("index_ML_type", ml_args (index_ml "type" ml_type)),
1.69 - ("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
1.70 - ("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
1.71 - ("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
1.72 - ("ML_functor", ThyOutput.args (Scan.lift Args.name) output_ml),
1.73 - ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)];
1.74 +val _ = index_ml "index_ML" "" ml_val;
1.75 +val _ = index_ml "index_ML_type" "type" ml_type;
1.76 +val _ = index_ml "index_ML_exn" "exception" ml_exn;
1.77 +val _ = index_ml "index_ML_structure" "structure" ml_structure;
1.78 +val _ = index_ml "index_ML_functor" "functor" ml_functor;
1.79
1.80 end;
1.81
1.82
1.83 -(* theorems with names *)
1.84 +(* named theorems *)
1.85
1.86 -local
1.87 +val _ = ThyOutput.antiquotation "named_thms"
1.88 + (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
1.89 + (fn {context = ctxt, ...} =>
1.90 + map (apfst (ThyOutput.pretty_thm ctxt))
1.91 + #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
1.92 + #> (if ! ThyOutput.display
1.93 + then
1.94 + map (fn (p, name) =>
1.95 + Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
1.96 + "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
1.97 + #> space_implode "\\par\\smallskip%\n"
1.98 + #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.99 + else
1.100 + map (fn (p, name) =>
1.101 + Output.output (Pretty.str_of p) ^
1.102 + "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
1.103 + #> space_implode "\\par\\smallskip%\n"
1.104 + #> enclose "\\isa{" "}"));
1.105
1.106 -fun output_named_thms src ctxt xs =
1.107 - map (apfst (ThyOutput.pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*)
1.108 - |> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
1.109 - |> (if ! ThyOutput.display then
1.110 - map (fn (p, name) =>
1.111 - Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
1.112 - "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
1.113 - #> space_implode "\\par\\smallskip%\n"
1.114 - #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.115 - else
1.116 - map (fn (p, name) =>
1.117 - Output.output (Pretty.str_of p) ^
1.118 - "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
1.119 - #> space_implode "\\par\\smallskip%\n"
1.120 - #> enclose "\\isa{" "}");
1.121
1.122 -in
1.123 +(* theory file *)
1.124
1.125 -val _ = ThyOutput.add_commands
1.126 - [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm --
1.127 - Scan.lift (Args.parens Args.name))) output_named_thms)];
1.128 +val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
1.129 + (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
1.130
1.131 -end;
1.132
1.133 -
1.134 -(* theory files *)
1.135 -
1.136 -val _ = ThyOutput.add_commands
1.137 - [("thy_file", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn name =>
1.138 - (ThyLoad.check_thy Path.current name; Pretty.str name))))];
1.139 -
1.140 -
1.141 -(* Isabelle entities (with index) *)
1.142 +(* Isabelle/Isar entities (with index) *)
1.143
1.144 local
1.145
1.146 @@ -147,56 +130,56 @@
1.147
1.148 val arg = enclose "{" "}" o clean_string;
1.149
1.150 -fun output_entity check markup index kind ctxt (logic, name) =
1.151 - let
1.152 - val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
1.153 - val hyper =
1.154 - enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
1.155 - index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
1.156 - val idx =
1.157 - (case index of
1.158 - NONE => ""
1.159 - | SOME is_def =>
1.160 - "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
1.161 - in
1.162 - if check ctxt name then
1.163 - idx ^
1.164 - (Output.output name
1.165 - |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
1.166 - |> (if ! ThyOutput.quotes then quote else I)
1.167 - |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.168 - else hyper o enclose "\\mbox{\\isa{" "}}"))
1.169 - else error ("Bad " ^ kind ^ " " ^ quote name)
1.170 - end;
1.171 -
1.172 -fun entity check markup index kind =
1.173 - ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
1.174 - (K (output_entity check markup index kind));
1.175 +fun entity check markup kind index =
1.176 + ThyOutput.antiquotation
1.177 + (case index of NONE => kind | SOME true => kind ^ "_def" | SOME false => kind ^ "_ref")
1.178 + (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
1.179 + (fn {context = ctxt, ...} => fn (logic, name) =>
1.180 + let
1.181 + val hyper_name =
1.182 + "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
1.183 + val hyper =
1.184 + enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
1.185 + index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
1.186 + val idx =
1.187 + (case index of
1.188 + NONE => ""
1.189 + | SOME is_def =>
1.190 + "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
1.191 + in
1.192 + if check ctxt name then
1.193 + idx ^
1.194 + (Output.output name
1.195 + |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
1.196 + |> (if ! ThyOutput.quotes then quote else I)
1.197 + |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.198 + else hyper o enclose "\\mbox{\\isa{" "}}"))
1.199 + else error ("Bad " ^ kind ^ " " ^ quote name)
1.200 + end);
1.201
1.202 fun entity_antiqs check markup kind =
1.203 - [(kind, entity check markup NONE kind),
1.204 - (kind ^ "_def", entity check markup (SOME true) kind),
1.205 - (kind ^ "_ref", entity check markup (SOME false) kind)];
1.206 + [(entity check markup kind NONE),
1.207 + (entity check markup kind (SOME true)),
1.208 + (entity check markup kind (SOME false))];
1.209
1.210 in
1.211
1.212 -val _ = ThyOutput.add_commands
1.213 - (entity_antiqs no_check "" "syntax" @
1.214 - entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
1.215 - entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @
1.216 - entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element" @
1.217 - entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
1.218 - entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
1.219 - entity_antiqs no_check "" "fact" @
1.220 - entity_antiqs no_check "" "variable" @
1.221 - entity_antiqs no_check "" "case" @
1.222 - entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
1.223 - entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
1.224 - entity_antiqs no_check "" "inference" @
1.225 - entity_antiqs no_check "isatt" "executable" @
1.226 - entity_antiqs (K check_tool) "isatt" "tool" @
1.227 - entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
1.228 - entity_antiqs (K ThyInfo.known_thy) "" "theory");
1.229 +val _ = entity_antiqs no_check "" "syntax";
1.230 +val _ = entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command";
1.231 +val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword";
1.232 +val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element";
1.233 +val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
1.234 +val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
1.235 +val _ = entity_antiqs no_check "" "fact";
1.236 +val _ = entity_antiqs no_check "" "variable";
1.237 +val _ = entity_antiqs no_check "" "case";
1.238 +val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
1.239 +val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
1.240 +val _ = entity_antiqs no_check "" "inference";
1.241 +val _ = entity_antiqs no_check "isatt" "executable";
1.242 +val _ = entity_antiqs (K check_tool) "isatt" "tool";
1.243 +val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
1.244 +val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
1.245
1.246 end;
1.247
2.1 --- a/doc-src/more_antiquote.ML Mon Mar 09 20:29:45 2009 +0100
2.2 +++ b/doc-src/more_antiquote.ML Mon Mar 09 20:34:11 2009 +0100
2.3 @@ -1,4 +1,4 @@
2.4 -(* Title: Doc/more_antiquote.ML
2.5 +(* Title: doc-src/more_antiquote.ML
2.6 Author: Florian Haftmann, TU Muenchen
2.7
2.8 More antiquotations.
2.9 @@ -12,15 +12,13 @@
2.10 structure More_Antiquote : MORE_ANTIQUOTE =
2.11 struct
2.12
2.13 -structure O = ThyOutput;
2.14 -
2.15 (* printing typewriter lines *)
2.16
2.17 fun typewriter s =
2.18 let
2.19 val parse = Scan.repeat
2.20 (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
2.21 - || (Scan.this_string " "
2.22 + || (Scan.this_string " "
2.23 || Scan.this_string "."
2.24 || Scan.this_string ","
2.25 || Scan.this_string ":"
2.26 @@ -66,9 +64,8 @@
2.27
2.28 in
2.29
2.30 -val _ = O.add_commands
2.31 - [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)),
2.32 - ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))]
2.33 +val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
2.34 +val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
2.35
2.36 end;
2.37
2.38 @@ -96,12 +93,12 @@
2.39 val thms = Code_Wellsorted.eqns funcgr const
2.40 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
2.41 |> map (holize o no_vars ctxt o AxClass.overload thy);
2.42 - in ThyOutput.output_list pretty_thm src ctxt thms end;
2.43 + in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
2.44
2.45 in
2.46
2.47 -val _ = O.add_commands
2.48 - [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
2.49 +val _ = ThyOutput.antiquotation "code_thms" Args.term
2.50 + (fn {source, context, ...} => pretty_code_thm source context);
2.51
2.52 end;
2.53
2.54 @@ -120,21 +117,20 @@
2.55 >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
2.56 val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
2.57 >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
2.58 - val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
2.59 -
2.60 - fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
2.61 - Code_Target.code_of (ProofContext.theory_of ctxt)
2.62 - target "Example" (mk_cs (ProofContext.theory_of ctxt))
2.63 - (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
2.64 - |> typewriter;
2.65 + val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
2.66
2.67 in
2.68
2.69 -val _ = O.add_commands
2.70 - [("code_stmts", O.args
2.71 - (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
2.72 - code_stmts)]
2.73 -
2.74 -end
2.75 +val _ = ThyOutput.antiquotation "code_stmts"
2.76 + (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
2.77 + (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
2.78 + let val thy = ProofContext.theory_of ctxt in
2.79 + Code_Target.code_of thy
2.80 + target "Example" (mk_cs thy)
2.81 + (fn naming => maps (fn f => f thy naming) mk_stmtss)
2.82 + |> typewriter
2.83 + end);
2.84
2.85 end;
2.86 +
2.87 +end;
3.1 --- a/src/Pure/Thy/thy_output.ML Mon Mar 09 20:29:45 2009 +0100
3.2 +++ b/src/Pure/Thy/thy_output.ML Mon Mar 09 20:34:11 2009 +0100
3.3 @@ -590,8 +590,9 @@
3.4
3.5 val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
3.6 val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
3.7 -val _ = ml_text "ML_struct"
3.8 - (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
3.9 +val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
3.10 +val _ = ml_text "ML_functor" (K ""); (*no check!*)
3.11 +val _ = ml_text "ML_text" (K "");
3.12
3.13 end;
3.14