proper Args.syntax for slightly odd bundle trickery;
authorwenzelm
Mon Mar 10 21:40:39 2014 +0100 (2014-03-10)
changeset 56035745f568837f1
parent 56034 1c59b555ac4a
child 56036 6c3fc3b5592a
proper Args.syntax for slightly odd bundle trickery;
do not handle arbitrary exceptions;
more abstract type Args.src;
src/HOL/Tools/Lifting/lifting_setup.ML
src/Pure/Isar/args.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 21:15:29 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 21:40:39 2014 +0100
     1.3 @@ -958,12 +958,10 @@
     1.4    in
     1.5      case bundle of
     1.6        [(_, [arg_src])] => 
     1.7 -        (let
     1.8 -          val tokens = Args.args_of_src arg_src
     1.9 -        in
    1.10 -          (fst (Args.name tokens))
    1.11 -          handle _ => error "The provided bundle is not a lifting bundle."
    1.12 -        end)
    1.13 +        let
    1.14 +          val (name, _) = Args.syntax (Scan.lift Args.name) arg_src ctxt
    1.15 +            handle ERROR _ => error "The provided bundle is not a lifting bundle."
    1.16 +        in name end
    1.17        | _ => error "The provided bundle is not a lifting bundle."
    1.18    end
    1.19  
     2.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 21:15:29 2014 +0100
     2.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 21:40:39 2014 +0100
     2.3 @@ -10,7 +10,6 @@
     2.4    type src
     2.5    val src: xstring * Position.T -> Token.T list -> src
     2.6    val name_of_src: src -> string * Position.T
     2.7 -  val args_of_src: src -> Token.T list
     2.8    val range_of_src: src -> Position.T
     2.9    val unparse_src: src -> string list
    2.10    val pretty_src: Proof.context -> src -> Pretty.T