# HG changeset patch # User wenzelm # Date 1395089792 -3600 # Node ID 2666cd7d380cb872c2381650f622db574339f51f # Parent f998bdd4076382cd76c318d5d71dc58742f046b7# Parent 01fb1b35433b4f74f8da68c5d6cb33a4532c473a merged diff -r f998bdd40763 -r 2666cd7d380c src/Doc/IsarRef/Inner_Syntax.thy --- 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 \ theory"} \\ @{command_def "typed_print_translation"} & : & @{text "theory \ theory"} \\ @{command_def "print_ast_translation"} & : & @{text "theory \ 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 diff -r f998bdd40763 -r 2666cd7d380c src/Doc/antiquote_setup.ML --- 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; diff -r f998bdd40763 -r 2666cd7d380c src/Pure/ML/ml_syntax.ML --- 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 *)