# HG changeset patch
# User wenzelm
# Date 1327522254 -3600
# Node ID b03897da3c90c2b1a23ca4b8e88a2137b6679137
# Parent  9be4ff2dd91e07b17a71b76cb94f126b69a265d0
document antiquotations for ML infix operators;

diff -r 9be4ff2dd91e -r b03897da3c90 doc-src/IsarRef/Thy/Document_Preparation.thy
--- 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.
diff -r 9be4ff2dd91e -r b03897da3c90 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- 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.
diff -r 9be4ff2dd91e -r b03897da3c90 doc-src/antiquote_setup.ML
--- 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 #>
diff -r 9be4ff2dd91e -r b03897da3c90 src/Pure/Thy/thy_output.ML
--- 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;") #>