clarified Args.src: more abstract type, position refers to name only;
authorwenzelm
Mon Mar 10 16:30:07 2014 +0100 (2014-03-10)
changeset 560298bedca4bd5a3
parent 56028 422024102d9d
child 56030 ef2ffd622264
clarified Args.src: more abstract type, position refers to name only;
prefer self-contained Args.check_src;
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/recdef.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/parse_spec.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 15:30:29 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Mar 10 16:30:07 2014 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4      val dummy_thm = Thm.transfer thy Drule.dummy_thm
     1.5      val pointer = Outer_Syntax.scan Position.none bundle_name
     1.6      val restore_lifting_att = 
     1.7 -      ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
     1.8 +      ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
     1.9    in
    1.10      lthy 
    1.11        |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.12 @@ -959,7 +959,7 @@
    1.13      case bundle of
    1.14        [(_, [arg_src])] => 
    1.15          (let
    1.16 -          val ((_, tokens), _) = Args.dest_src arg_src
    1.17 +          val tokens = Args.args_of_src arg_src
    1.18          in
    1.19            (fst (Args.name tokens))
    1.20            handle _ => error "The provided bundle is not a lifting bundle."
     2.1 --- a/src/HOL/Tools/recdef.ML	Mon Mar 10 15:30:29 2014 +0100
     2.2 +++ b/src/HOL/Tools/recdef.ML	Mon Mar 10 16:30:07 2014 +0100
     2.3 @@ -290,7 +290,8 @@
     2.4  
     2.5  val hints =
     2.6    @{keyword "("} |--
     2.7 -    Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src;
     2.8 +    Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"})
     2.9 +  >> uncurry Args.src;
    2.10  
    2.11  val recdef_decl =
    2.12    Scan.optional
     3.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 15:30:29 2014 +0100
     3.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 16:30:07 2014 +0100
     3.3 @@ -8,11 +8,12 @@
     3.4  signature ARGS =
     3.5  sig
     3.6    type src
     3.7 -  val src: (string * Token.T list) * Position.T -> src
     3.8 -  val dest_src: src -> (string * Token.T list) * Position.T
     3.9 +  val src: xstring * Position.T -> Token.T list -> src
    3.10 +  val name_of_src: src -> string * Position.T
    3.11 +  val args_of_src: src -> Token.T list
    3.12    val unparse_src: src -> string list
    3.13    val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
    3.14 -  val map_name: (string -> string) -> src -> src
    3.15 +  val check_src: Context.generic -> 'a Name_Space.table -> src -> src * 'a
    3.16    val transform_values: morphism -> src -> src
    3.17    val init_assignable: src -> src
    3.18    val closure: src -> src
    3.19 @@ -75,12 +76,16 @@
    3.20  
    3.21  (** datatype src **)
    3.22  
    3.23 -datatype src = Src of (string * Token.T list) * Position.T;
    3.24 +datatype src = Src of (string * Position.T) * Token.T list;
    3.25 +
    3.26 +val src = curry Src;
    3.27  
    3.28 -val src = Src;
    3.29 -fun dest_src (Src src) = src;
    3.30 +fun map_args f (Src (name, args)) = Src (name, map f args);
    3.31  
    3.32 -fun unparse_src (Src ((_, toks), _)) = map Token.unparse toks;
    3.33 +fun name_of_src (Src (name, _)) = name;
    3.34 +fun args_of_src (Src (_, args)) = args;
    3.35 +
    3.36 +fun unparse_src (Src (_, args)) = map Token.unparse args;
    3.37  
    3.38  fun pretty_src pretty_name ctxt src =
    3.39    let
    3.40 @@ -93,11 +98,15 @@
    3.41        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    3.42        | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    3.43        | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    3.44 -    val (name, args) = #1 (dest_src src);
    3.45 +    val Src ((name, _), args) = src;
    3.46    in Pretty.block (Pretty.breaks (pretty_name name :: map prt args)) end;
    3.47  
    3.48 -fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
    3.49 -fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
    3.50 +
    3.51 +(* check *)
    3.52 +
    3.53 +fun check_src context table (Src ((xname, pos), args)) =
    3.54 +  let val (name, x) = Name_Space.check context table (xname, pos)
    3.55 +  in (Src ((name, pos), args), x) end;
    3.56  
    3.57  
    3.58  (* values *)
    3.59 @@ -268,7 +277,7 @@
    3.60    let
    3.61      fun intern tok = check (Token.content_of tok, Token.pos_of tok);
    3.62      val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
    3.63 -    val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
    3.64 +    val attrib = Parse.position attrib_name -- Parse.!!! parse >> uncurry src;
    3.65    in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
    3.66  
    3.67  fun opt_attribs check = Scan.optional (attribs check) [];
    3.68 @@ -287,7 +296,7 @@
    3.69  
    3.70  (** syntax wrapper **)
    3.71  
    3.72 -fun syntax kind scan (Src ((s, args0), pos)) context =
    3.73 +fun syntax kind scan (Src ((name, pos), args0)) context =
    3.74    let
    3.75      val args1 = map Token.init_assignable args0;
    3.76      fun reported_text () =
    3.77 @@ -300,7 +309,7 @@
    3.78      (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
    3.79        (SOME x, (context', [])) => (Output.report (reported_text ()); (x, context'))
    3.80      | (_, (_, args2)) =>
    3.81 -        error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
    3.82 +        error ("Bad arguments for " ^ kind ^ " " ^ quote name ^ Position.here pos ^
    3.83            (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
    3.84            Markup.markup_report (reported_text ())))
    3.85    end;
     4.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 10 15:30:29 2014 +0100
     4.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 16:30:07 2014 +0100
     4.3 @@ -118,12 +118,7 @@
     4.4  (* check *)
     4.5  
     4.6  fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
     4.7 -
     4.8 -fun check_src_generic context src =
     4.9 -  let
    4.10 -    val ((xname, toks), pos) = Args.dest_src src;
    4.11 -    val name = check_name_generic context (xname, pos);
    4.12 -  in Args.src ((name, toks), pos) end;
    4.13 +fun check_src_generic context src = #1 (Args.check_src context (get_attributes context) src);
    4.14  
    4.15  val check_name = check_name_generic o Context.Proof;
    4.16  val check_src = check_src_generic o Context.Proof;
    4.17 @@ -141,13 +136,8 @@
    4.18  (* get attributes *)
    4.19  
    4.20  fun attribute_generic context =
    4.21 -  let val table = get_attributes context in
    4.22 -    fn src =>
    4.23 -      let
    4.24 -        val ((name, _), _) = Args.dest_src src;
    4.25 -        val (att, _) = Name_Space.get table name;
    4.26 -      in att src end
    4.27 -  end;
    4.28 +  let val table = get_attributes context
    4.29 +  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
    4.30  
    4.31  val attribute = attribute_generic o Context.Proof;
    4.32  val attribute_global = attribute_generic o Context.Theory;
    4.33 @@ -201,7 +191,7 @@
    4.34  
    4.35  (* internal attribute *)
    4.36  
    4.37 -fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
    4.38 +fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
    4.39  
    4.40  val _ = Theory.setup
    4.41   (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
    4.42 @@ -273,7 +263,7 @@
    4.43    in (src2, result) end;
    4.44  
    4.45  fun err msg src =
    4.46 -  let val ((name, _), pos) = Args.dest_src src
    4.47 +  let val (name, pos) = Args.name_of_src src
    4.48    in error (msg ^ " " ^ quote name ^ Position.here pos) end;
    4.49  
    4.50  fun eval src ((th, dyn), (decls, context)) =
     5.1 --- a/src/Pure/Isar/method.ML	Mon Mar 10 15:30:29 2014 +0100
     5.2 +++ b/src/Pure/Isar/method.ML	Mon Mar 10 16:30:07 2014 +0100
     5.3 @@ -300,7 +300,7 @@
     5.4  
     5.5  fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
     5.6  val succeed_text = Basic (K succeed);
     5.7 -val default_text = Source (Args.src (("default", []), Position.none));
     5.8 +val default_text = Source (Args.src ("default", Position.none) []);
     5.9  val this_text = Basic (K this);
    5.10  val done_text = Basic (K (SIMPLE_METHOD all_tac));
    5.11  fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
    5.12 @@ -340,24 +340,14 @@
    5.13  (* check *)
    5.14  
    5.15  fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
    5.16 -
    5.17 -fun check_src ctxt src =
    5.18 -  let
    5.19 -    val ((xname, toks), pos) = Args.dest_src src;
    5.20 -    val name = check_name ctxt (xname, pos);
    5.21 -  in Args.src ((name, toks), pos) end;
    5.22 +fun check_src ctxt src = #1 (Args.check_src (Context.Proof ctxt) (get_methods ctxt) src);
    5.23  
    5.24  
    5.25  (* get methods *)
    5.26  
    5.27  fun method ctxt =
    5.28 -  let val table = get_methods ctxt in
    5.29 -    fn src =>
    5.30 -      let
    5.31 -        val ((name, _), _) = Args.dest_src src;
    5.32 -        val (meth, _) = Name_Space.get table name;
    5.33 -      in meth src end
    5.34 -  end;
    5.35 +  let val table = get_methods ctxt
    5.36 +  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
    5.37  
    5.38  fun method_cmd ctxt = method ctxt o check_src ctxt;
    5.39  
    5.40 @@ -456,9 +446,9 @@
    5.41  local
    5.42  
    5.43  fun meth4 x =
    5.44 - (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
    5.45 + (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) ||
    5.46    Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
    5.47 -    Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
    5.48 +    Source (Args.src ("cartouche", Token.pos_of tok) [tok])) ||
    5.49    Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
    5.50  and meth3 x =
    5.51   (meth4 -- Parse.position (Parse.$$$ "?")
    5.52 @@ -471,7 +461,7 @@
    5.53          Select_Goals (combinator_info [pos1, pos2], n, m)) ||
    5.54    meth4) x
    5.55  and meth2 x =
    5.56 - (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
    5.57 + (Parse.position Parse.xname -- Args.parse1 is_symid_meth >> (Source o uncurry Args.src) ||
    5.58    meth3) x
    5.59  and meth1 x =
    5.60    (Parse.enum1_positions "," meth2
     6.1 --- a/src/Pure/Isar/parse_spec.ML	Mon Mar 10 15:30:29 2014 +0100
     6.2 +++ b/src/Pure/Isar/parse_spec.ML	Mon Mar 10 16:30:07 2014 +0100
     6.3 @@ -37,7 +37,7 @@
     6.4  
     6.5  (* theorem specifications *)
     6.6  
     6.7 -val attrib = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src;
     6.8 +val attrib = Parse.position Parse.liberal_name -- Parse.!!! Args.parse >> uncurry Args.src;
     6.9  val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
    6.10  val opt_attribs = Scan.optional attribs [];
    6.11  
     7.1 --- a/src/Pure/ML/ml_context.ML	Mon Mar 10 15:30:29 2014 +0100
     7.2 +++ b/src/Pure/ML/ml_context.ML	Mon Mar 10 16:30:07 2014 +0100
     7.3 @@ -115,10 +115,8 @@
     7.4  fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
     7.5  
     7.6  fun antiquotation src ctxt =
     7.7 -  let
     7.8 -    val ((xname, _), pos) = Args.dest_src src;
     7.9 -    val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos);
    7.10 -  in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
    7.11 +  let val (src', scan) = Args.check_src (Context.Proof ctxt) (get_antiqs ctxt) src
    7.12 +  in Args.context_syntax Markup.ML_antiquotationN scan src' ctxt end;
    7.13  
    7.14  
    7.15  (* parsing and evaluation *)
    7.16 @@ -127,7 +125,7 @@
    7.17  
    7.18  val antiq =
    7.19    Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
    7.20 -  >> (fn ((x, pos), y) => Args.src ((x, y), pos));
    7.21 +  >> uncurry Args.src;
    7.22  
    7.23  val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
    7.24  
     8.1 --- a/src/Pure/Thy/term_style.ML	Mon Mar 10 15:30:29 2014 +0100
     8.2 +++ b/src/Pure/Thy/term_style.ML	Mon Mar 10 16:30:07 2014 +0100
     8.3 @@ -42,10 +42,10 @@
     8.4  
     8.5  (* style parsing *)
     8.6  
     8.7 -fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
     8.8 -  >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
     8.9 +fun parse_single ctxt = Parse.position Parse.xname -- Args.parse
    8.10 +  >> (fn ((name, pos), args) => fst (Args.context_syntax "style"
    8.11         (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
    8.12 -         (Args.src x) ctxt |>> (fn f => f ctxt)));
    8.13 +         (Args.src (name, pos) args) ctxt |>> (fn f => f ctxt)));
    8.14  
    8.15  val parse = Args.context :|-- (fn ctxt => Scan.lift
    8.16    (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
     9.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:30:29 2014 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 16:30:07 2014 +0100
     9.3 @@ -92,11 +92,8 @@
     9.4  fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
     9.5  
     9.6  fun command src state ctxt =
     9.7 -  let
     9.8 -    val ((xname, _), pos) = Args.dest_src src;
     9.9 -    val (name, f) =
    9.10 -      Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
    9.11 -  in f src state ctxt end;
    9.12 +  let val (src', f) = Args.check_src (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) src
    9.13 +  in f src' state ctxt end;
    9.14  
    9.15  fun option ((xname, pos), s) ctxt =
    9.16    let
    9.17 @@ -155,7 +152,7 @@
    9.18  val antiq =
    9.19    Parse.!!!
    9.20      (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
    9.21 -  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
    9.22 +  >> (fn ((name, props), args) => (props, Args.src name args));
    9.23  
    9.24  end;
    9.25  
    9.26 @@ -615,12 +612,11 @@
    9.27  
    9.28  val _ = Theory.setup
    9.29    (antiquotation (Binding.name "lemma")
    9.30 -    (Args.prop --
    9.31 +    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
    9.32        Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
    9.33 -    (fn {source, context = ctxt, ...} => fn (prop, (((_, by_pos), m1), m2)) =>
    9.34 +    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
    9.35        let
    9.36 -        val prop_src =
    9.37 -          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
    9.38 +        val prop_src = Args.src (Args.name_of_src source) [prop_token];
    9.39  
    9.40          val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
    9.41          val _ = Context_Position.reports ctxt reports;