--- a/src/Doc/IsarRef/Inner_Syntax.thy Mon Mar 17 20:38:50 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Mon Mar 17 21:56:32 2014 +0100
@@ -1453,10 +1453,10 @@
@{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
- @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
- @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
- @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
- @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
+ @{ML_antiquotation_def "class_syntax"} & : & @{text "ML antiquotation"} \\
+ @{ML_antiquotation_def "type_syntax"} & : & @{text "ML antiquotation"} \\
+ @{ML_antiquotation_def "const_syntax"} & : & @{text "ML antiquotation"} \\
+ @{ML_antiquotation_def "syntax_const"} & : & @{text "ML antiquotation"} \\
\end{matharray}
Syntax translation functions written in ML admit almost arbitrary
--- a/src/Doc/antiquote_setup.ML Mon Mar 17 20:38:50 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Mon Mar 17 21:56:32 2014 +0100
@@ -190,7 +190,7 @@
fun no_check _ _ = true;
-fun command_check (name, pos) =
+fun check_command (name, pos) =
is_some (Keyword.command_keyword name) andalso
let
val markup =
@@ -213,13 +213,14 @@
val arg = enclose "{" "}" o clean_string;
-fun entity check markup kind index =
+fun entity check markup binding index =
Thy_Output.antiquotation
- (Binding.name (translate (fn " " => "_" | c => c) kind ^
+ (binding |> Binding.map_name (fn name => name ^
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
(fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
let
+ val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
val hyper_name =
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
val hyper =
@@ -251,24 +252,24 @@
val _ =
Theory.setup
- (entity_antiqs no_check "" "syntax" #>
- entity_antiqs (K command_check) "isacommand" "command" #>
- entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
- entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
- entity_antiqs (can o Method.check_name) "" "method" #>
- entity_antiqs (can o Attrib.check_name) "" "attribute" #>
- entity_antiqs no_check "" "fact" #>
- entity_antiqs no_check "" "variable" #>
- entity_antiqs no_check "" "case" #>
- entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
- entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
- entity_antiqs no_check "isatt" "setting" #>
- entity_antiqs no_check "isatt" "system option" #>
- entity_antiqs no_check "" "inference" #>
- entity_antiqs no_check "isatt" "executable" #>
- entity_antiqs (K check_tool) "isatool" "tool" #>
- entity_antiqs (can o ML_Context.check_antiquotation) "" Markup.ML_antiquotationN #>
- entity_antiqs (K (is_action o #1)) "isatt" "action");
+ (entity_antiqs no_check "" @{binding syntax} #>
+ entity_antiqs (K check_command) "isacommand" @{binding command} #>
+ entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
+ entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
+ entity_antiqs (can o Method.check_name) "" @{binding method} #>
+ entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
+ entity_antiqs no_check "" @{binding fact} #>
+ entity_antiqs no_check "" @{binding variable} #>
+ entity_antiqs no_check "" @{binding case} #>
+ entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
+ entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
+ entity_antiqs no_check "isatt" @{binding setting} #>
+ entity_antiqs no_check "isatt" @{binding system_option} #>
+ entity_antiqs no_check "" @{binding inference} #>
+ entity_antiqs no_check "isatt" @{binding executable} #>
+ entity_antiqs (K check_tool) "isatool" @{binding tool} #>
+ entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
+ entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
end;
--- a/src/Pure/ML/ml_syntax.ML Mon Mar 17 20:38:50 2014 +0100
+++ b/src/Pure/ML/ml_syntax.ML Mon Mar 17 21:56:32 2014 +0100
@@ -85,17 +85,17 @@
val print_class = print_string;
val print_sort = print_list print_class;
-fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
- | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
- | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
+fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg
+ | print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg
+ | print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg;
-fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
- | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
- | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
- | print_term (Bound i) = "Bound " ^ print_int i
+fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg
+ | print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg
+ | print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg
+ | print_term (Bound i) = "Term.Bound " ^ print_int i
| print_term (Abs (s, T, t)) =
- "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
- | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
+ "Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
+ | print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2);
(* toplevel pretty printing *)