src/Pure/Isar/args.ML
changeset 56200 1f9951be72b5
parent 56063 38f13d055107
child 56201 dd2df97b379b
equal deleted inserted replaced
56199:8e8d28ed7529 56200:1f9951be72b5
    63   val goal_spec: ((int -> tactic) -> tactic) context_parser
    63   val goal_spec: ((int -> tactic) -> tactic) context_parser
    64   val parse: Token.T list parser
    64   val parse: Token.T list parser
    65   val parse1: (string -> bool) -> Token.T list parser
    65   val parse1: (string -> bool) -> Token.T list parser
    66   val attribs: (xstring * Position.T -> string) -> src list parser
    66   val attribs: (xstring * Position.T -> string) -> src list parser
    67   val opt_attribs: (xstring * Position.T -> string) -> src list parser
    67   val opt_attribs: (xstring * Position.T -> string) -> src list parser
    68   val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
       
    69   val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
       
    70   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
    68   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
    71   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    69   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    72 end;
    70 end;
    73 
    71 
    74 structure Args: ARGS =
    72 structure Args: ARGS =
   300     val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
   298     val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
   301     val attrib = Parse.position attrib_name -- Parse.!!! parse >> uncurry src;
   299     val attrib = Parse.position attrib_name -- Parse.!!! parse >> uncurry src;
   302   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
   300   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
   303 
   301 
   304 fun opt_attribs check = Scan.optional (attribs check) [];
   302 fun opt_attribs check = Scan.optional (attribs check) [];
   305 
       
   306 
       
   307 (* theorem specifications *)
       
   308 
       
   309 fun thm_name check_attrib s = binding -- opt_attribs check_attrib --| $$$ s;
       
   310 
       
   311 fun opt_thm_name check_attrib s =
       
   312   Scan.optional
       
   313     ((binding -- opt_attribs check_attrib || attribs check_attrib >> pair Binding.empty) --| $$$ s)
       
   314     (Binding.empty, []);
       
   315 
   303 
   316 
   304 
   317 
   305 
   318 (** syntax wrapper **)
   306 (** syntax wrapper **)
   319 
   307