--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Wed Jan 25 20:26:05 2012 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Wed Jan 25 21:10:54 2012 +0100
@@ -155,6 +155,7 @@
@{antiquotation_def prf} & : & @{text antiquotation} \\
@{antiquotation_def full_prf} & : & @{text antiquotation} \\
@{antiquotation_def ML} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_op} & : & @{text antiquotation} \\
@{antiquotation_def ML_type} & : & @{text antiquotation} \\
@{antiquotation_def ML_struct} & : & @{text antiquotation} \\
@{antiquotation_def "file"} & : & @{text antiquotation} \\
@@ -197,12 +198,15 @@
@@{antiquotation typ} options @{syntax type} |
@@{antiquotation type} options @{syntax name} |
@@{antiquotation class} options @{syntax name} |
- @@{antiquotation text} options @{syntax name} |
+ @@{antiquotation text} options @{syntax name}
+ ;
+ @{syntax antiquotation}:
@@{antiquotation goals} options |
@@{antiquotation subgoals} options |
@@{antiquotation prf} options @{syntax thmrefs} |
@@{antiquotation full_prf} options @{syntax thmrefs} |
@@{antiquotation ML} options @{syntax name} |
+ @@{antiquotation ML_op} options @{syntax name} |
@@{antiquotation ML_type} options @{syntax name} |
@@{antiquotation ML_struct} options @{syntax name} |
@@{antiquotation \"file\"} options @{syntax name}
@@ -289,9 +293,10 @@
information omitted in the compact proof term, which is denoted by
``@{text _}'' placeholders there.
- \item @{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
- "@{ML_struct s}"} check text @{text s} as ML value, type, and
- structure, respectively. The source is printed verbatim.
+ \item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type
+ s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value,
+ infix operator, type, and structure, respectively. The source is
+ printed verbatim.
\item @{text "@{file path}"} checks that @{text "path"} refers to a
file (or directory) and prints it verbatim.
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Wed Jan 25 20:26:05 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Wed Jan 25 21:10:54 2012 +0100
@@ -205,6 +205,7 @@
\indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
+ \indexdef{}{antiquotation}{ML\_op}\hypertarget{antiquotation.ML-op}{\hyperlink{antiquotation.ML-op}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}op}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{file}\hypertarget{antiquotation.file}{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}} & : & \isa{antiquotation} \\
@@ -236,7 +237,7 @@
\rail@nont{\isa{antiquotation}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
-\rail@begin{23}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
+\rail@begin{15}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
\rail@bar
\rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
\rail@nont{\isa{options}}[]
@@ -305,33 +306,40 @@
\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{15}
+\rail@endbar
+\rail@end
+\rail@begin{9}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}
+\rail@bar
\rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{16}
+\rail@nextbar{1}
\rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{17}
+\rail@nextbar{2}
\rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{18}
+\rail@nextbar{3}
\rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{19}
+\rail@nextbar{4}
\rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{20}
+\rail@nextbar{5}
+\rail@term{\hyperlink{antiquotation.ML-op}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}op}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nextbar{6}
\rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{21}
+\rail@nextbar{7}
\rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{22}
+\rail@nextbar{8}
\rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -445,8 +453,9 @@
information omitted in the compact proof term, which is denoted by
``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' placeholders there.
- \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}type\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}struct\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} check text \isa{s} as ML value, type, and
- structure, respectively. The source is printed verbatim.
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}op\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}type\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}struct\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} check text \isa{s} as ML value,
+ infix operator, type, and structure, respectively. The source is
+ printed verbatim.
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}file\ path{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} checks that \isa{{\isaliteral{22}{\isachardoublequote}}path{\isaliteral{22}{\isachardoublequote}}} refers to a
file (or directory) and prints it verbatim.
--- a/doc-src/antiquote_setup.ML Wed Jan 25 20:26:05 2012 +0100
+++ b/doc-src/antiquote_setup.ML Wed Jan 25 21:10:54 2012 +0100
@@ -52,6 +52,9 @@
fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");"
| ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ ");";
+fun ml_op (txt1, "") = "fn _ => (op " ^ txt1 ^ ");"
+ | ml_op (txt1, txt2) = "fn _ => (op " ^ txt1 ^ " : " ^ txt2 ^ ");";
+
fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
| ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
@@ -95,6 +98,7 @@
val index_ml_setup =
index_ml @{binding index_ML} "" ml_val #>
+ index_ml @{binding index_ML_op} "infix" ml_op #>
index_ml @{binding index_ML_type} "type" ml_type #>
index_ml @{binding index_ML_exn} "exception" ml_exn #>
index_ml @{binding index_ML_structure} "structure" ml_structure #>
--- a/src/Pure/Thy/thy_output.ML Wed Jan 25 20:26:05 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Jan 25 21:10:54 2012 +0100
@@ -670,6 +670,7 @@
val _ =
Context.>> (Context.map_theory
(ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
+ ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
ml_text (Binding.name "ML_struct")
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>