doc-src/antiquote_setup.ML
changeset 46261 b03897da3c90
parent 45675 ac54a3abff81
child 46518 11b6471c2f50
     1.1 --- a/doc-src/antiquote_setup.ML	Wed Jan 25 20:26:05 2012 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed Jan 25 21:10:54 2012 +0100
     1.3 @@ -52,6 +52,9 @@
     1.4  fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");"
     1.5    | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ ");";
     1.6  
     1.7 +fun ml_op (txt1, "") = "fn _ => (op " ^ txt1 ^ ");"
     1.8 +  | ml_op (txt1, txt2) = "fn _ => (op " ^ txt1 ^ " : " ^ txt2 ^ ");";
     1.9 +
    1.10  fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
    1.11    | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
    1.12  
    1.13 @@ -95,6 +98,7 @@
    1.14  
    1.15  val index_ml_setup =
    1.16    index_ml @{binding index_ML} "" ml_val #>
    1.17 +  index_ml @{binding index_ML_op} "infix" ml_op #>
    1.18    index_ml @{binding index_ML_type} "type" ml_type #>
    1.19    index_ml @{binding index_ML_exn} "exception" ml_exn #>
    1.20    index_ml @{binding index_ML_structure} "structure" ml_structure #>