Lines Matching defs:name
190 Parse.name -- Scan.optional
380 ("attribute_setup",Parse.position Parse.name -- (* line 309 *)
384 ("method_setup",Parse.position Parse.name -- (* line 315 *)
395 Parse.position Parse.name --
410 ("oracle", Parse.position Parse.name --
492 (Parse.name || @{keyword "["} || @{keyword "("})
591 (let val p = Scan.repeat1 (Parse.name --| (* line 493 *)
626 (let val {name = (name, _), imports, uses, ...} = header
628 val _ = Present.init_theory name
758 fun format_type_mixfix name mx nargs =
760 Mixfix.syn_ext_types [(name,Mixfix.make_type nargs,mx)]
765 fun format_const_mixfix state name mx tp =
769 [(name,case tp of
787 fun attr (name : string) (f : 'a -> string) (v : 'a) =
788 [(name,f v)];
789 fun a (name : string) (v : string) = attr name I v;
790 fun attr_of_option (vname : string) (name : string) (f : 'a -> string)
791 = variant vname (K "") [fn SOME v' => attr name f v',
793 fun xml name attrs body = XML.Elem ((name,attrs),body);
794 fun xml' name body attrs = xml name attrs body;
815 val xml_of_import = attr "name" #1 #> xml' "Import" [];
817 [fn (s,SOME ((s1,[]),[])) => a "name" ("\""^s^"\" :: "^s1),
818 fn (s,NONE) => a "name" s] #> xml' "Keyword" [];
819 fun xml_of_use (p,b) = xml "UseFile" (attr "name"
822 [fn ((name,_),(("",false),Expression.Named [])) =>
823 a "name" name] #> xml' "Parent" [];
850 val attr_of_binding = attr "name" string_of_binding;
851 fun attrs_of_binding state (name,args) =
852 attr_of_binding name@
868 fun format_mixfix state name tp = variant "format_mixfix"
871 fn mx => Parser.format_const_mixfix state name mx tp
873 fun format_type_mixfix name num_args = variant
876 fn mx => Parser.format_type_mixfix name mx num_args
878 fun xml_of_mixfix state name tp mx =
879 case format_mixfix state name tp mx of
887 fun xml_of_type_mixfix name mx num_args =
888 case format_type_mixfix name num_args mx of
900 (let val name = string_of_binding b
901 val tp = Parser.inferred_param name state target
903 xml_of_mixfix state name (SOME tp) mx end)) fixes
935 val (name,tp) = dest_Free c
936 val old = Symtab.lookup t name
939 Symtab.update (name,(tp,def_tms@
941 |NONE => Symtab.update (name,(tp,
957 val elem = xml "FixrecFun" (a "name" b)
974 val (name,tp) = dest_Const c
975 val old = Symtab.lookup t name
978 Symtab.update (name,(tp,def_tms@
980 |NONE => Symtab.update (name,(tp,
992 val elem = xml "Fun" (a "name" b)
998 fun xml_of_statement state target name =
1003 attr_of_binding name
1022 (List.map (fn n => xml "class" (a "name" n) []) s)
1028 let val l' = List.map (fn ((name,tm),args) =>
1036 in xml "Def" (a "args" args'@attr_of_binding name@
1044 let val vars' = List.map (fn (name,sort) => case sort of
1045 SOME sort' => TFree (name,
1047 |NONE => TFree (name,[])) vars
1063 let val ([name],args',sort) = Class.read_multi_arity
1071 in (xml "Instantiation" (a "type" name)
1100 fn Locale ((name,(parents,ctxt)),body) =>
1109 val name' = attr_of_binding name
1110 val target = SOME (string_of_binding name,Position.none)
1113 in (xml "Locale" name' (ctxt'::parents'@
1115 fn Class ((name,(parents,ctxt)),body) =>
1121 val target = SOME (string_of_binding name,Position.none)
1122 val parents' = List.map (attr "name"
1127 val name' = attr_of_binding name
1130 in (xml "Cls" name' (ctxt'::parents'@
1132 fn TypeSynonym (((target,vars),name),(typ,mx))
1137 val name' = attr_of_binding name
1139 val mx' = xml_of_type_mixfix (string_of_binding name)
1144 in (xml "TypeSynonym" (name'@target')
1149 (fn ((name,vars,mx),cs) => xml "Datatype"
1150 (attr_of_binding name)
1151 (xml_of_type_mixfix (string_of_binding name)
1158 (string_of_binding name,
1180 (fn (name,tp,mx) =>
1182 val name' = string_of_binding name
1183 val mx' = xml_of_mixfix state name' (SOME tp') mx
1184 in xml "ConstDef" [("name",name')]
1192 fn Lemma ((((target,(name,args)), strs),(ctxt,stmt)),proof) =>
1200 @xml_of_statement state target name stmt),s1) end
1204 fn Definition (target,(name,(binding,tm))) =>
1211 Specification.read_free_spec (the_list name)
1215 val (((name',tp),vs),def_tm) = tm'' |>
1221 val mx' = case name of
1222 SOME (_,_,mx) => xml_of_mixfix state name' (SOME tp)
1225 in (xml "Definition" (a "name" name'@
1244 val dts' = List.map (fn (((vs,name),mx), cs) =>
1250 name) mx (List.length vs)
1267 in xml "Domain" (attr_of_binding name)
1294 val name = attr "name" #1 (#name h)
1304 in thys@[xml "Thy" (name@header') (imports@keywords@body')] end;