clarified Args.check_src: retain name space information for error output;
authorwenzelm
Mon Mar 10 18:06:23 2014 +0100 (2014-03-10)
changeset 56032b034b9f0fa2a
parent 56031 2e3329b89383
child 56033 513c2b0ea565
clarified Args.check_src: retain name space information for error output;
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.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/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 17:52:30 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 18:06:23 2014 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4    let
     1.5      val ths = Attrib.eval_thms ctxt [xthm]
     1.6      val bracket =
     1.7 -      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str ctxt) args
     1.8 +      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
     1.9        |> implode
    1.10      fun nth_name j =
    1.11        (case xref of
     2.1 --- a/src/HOL/Tools/recdef.ML	Mon Mar 10 17:52:30 2014 +0100
     2.2 +++ b/src/HOL/Tools/recdef.ML	Mon Mar 10 18:06:23 2014 +0100
     2.3 @@ -164,7 +164,7 @@
     2.4      val ctxt =
     2.5        (case opt_src of
     2.6          NONE => ctxt0
     2.7 -      | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
     2.8 +      | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
     2.9      val {simps, congs, wfs} = get_hints ctxt;
    2.10      val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
    2.11    in (ctxt', rev (map snd congs), wfs) end;
     3.1 --- a/src/HOL/Tools/try0.ML	Mon Mar 10 17:52:30 2014 +0100
     3.2 +++ b/src/HOL/Tools/try0.ML	Mon Mar 10 18:06:23 2014 +0100
     3.3 @@ -172,7 +172,7 @@
     3.4  
     3.5  fun string_of_xthm (xref, args) =
     3.6    Facts.string_of_ref xref ^
     3.7 -  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str @{context}) args);
     3.8 +  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
     3.9  
    3.10  val parse_fact_refs =
    3.11    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
     4.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 17:52:30 2014 +0100
     4.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 18:06:23 2014 +0100
     4.3 @@ -12,8 +12,8 @@
     4.4    val name_of_src: src -> string * Position.T
     4.5    val args_of_src: src -> Token.T list
     4.6    val unparse_src: src -> string list
     4.7 -  val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
     4.8 -  val check_src: Context.generic -> 'a Name_Space.table -> src -> src * 'a
     4.9 +  val pretty_src: Proof.context -> src -> Pretty.T
    4.10 +  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
    4.11    val transform_values: morphism -> src -> src
    4.12    val init_assignable: src -> src
    4.13    val closure: src -> src
    4.14 @@ -67,8 +67,8 @@
    4.15    val opt_attribs: (xstring * Position.T -> string) -> src list parser
    4.16    val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
    4.17    val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
    4.18 -  val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
    4.19 -  val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    4.20 +  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
    4.21 +  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    4.22  end;
    4.23  
    4.24  structure Args: ARGS =
    4.25 @@ -76,18 +76,28 @@
    4.26  
    4.27  (** datatype src **)
    4.28  
    4.29 -datatype src = Src of (string * Position.T) * Token.T list;
    4.30 +datatype src =
    4.31 +  Src of
    4.32 +   {name: string * Position.T,
    4.33 +    args: Token.T list,
    4.34 +    output_info: (string * Markup.T) option};
    4.35  
    4.36 -val src = curry Src;
    4.37 +fun src name args = Src {name = name, args = args, output_info = NONE};
    4.38  
    4.39 -fun map_args f (Src (name, args)) = Src (name, map f args);
    4.40 +fun map_args f (Src {name, args, output_info}) =
    4.41 +  Src {name = name, args = map f args, output_info = output_info};
    4.42  
    4.43 -fun name_of_src (Src (name, _)) = name;
    4.44 -fun args_of_src (Src (_, args)) = args;
    4.45 +fun name_of_src (Src {name, ...}) = name;
    4.46 +fun args_of_src (Src {args, ...}) = args;
    4.47 +
    4.48 +fun unparse_src (Src {args, ...}) = map Token.unparse args;
    4.49  
    4.50 -fun unparse_src (Src (_, args)) = map Token.unparse args;
    4.51 +fun pretty_name (Src {name = (name, _), output_info, ...}) =
    4.52 +  (case output_info of
    4.53 +    NONE => Pretty.str name
    4.54 +  | SOME (_, markup) => Pretty.mark_str (markup, name));
    4.55  
    4.56 -fun pretty_src pretty_name ctxt src =
    4.57 +fun pretty_src ctxt src =
    4.58    let
    4.59      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    4.60      fun prt arg =
    4.61 @@ -98,15 +108,18 @@
    4.62        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    4.63        | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    4.64        | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    4.65 -    val Src ((name, _), args) = src;
    4.66 -  in Pretty.block (Pretty.breaks (pretty_name name :: map prt args)) end;
    4.67 +  in Pretty.block (Pretty.breaks (pretty_name src :: map prt (args_of_src src))) end;
    4.68  
    4.69  
    4.70  (* check *)
    4.71  
    4.72 -fun check_src context table (Src ((xname, pos), args)) =
    4.73 -  let val (name, x) = Name_Space.check context table (xname, pos)
    4.74 -  in (Src ((name, pos), args), x) end;
    4.75 +fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
    4.76 +  let
    4.77 +    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
    4.78 +    val space = Name_Space.space_of_table table;
    4.79 +    val kind = Name_Space.kind_of space;
    4.80 +    val markup = Name_Space.markup space name;
    4.81 +  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
    4.82  
    4.83  
    4.84  (* values *)
    4.85 @@ -296,9 +309,13 @@
    4.86  
    4.87  (** syntax wrapper **)
    4.88  
    4.89 -fun syntax kind scan (Src ((name, pos), args0)) context =
    4.90 +fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
    4.91    let
    4.92      val args1 = map Token.init_assignable args0;
    4.93 +    fun print_name () =
    4.94 +      (case output_info of
    4.95 +        NONE => quote name
    4.96 +      | SOME (kind, markup) => kind ^ " " ^ Markup.markup markup (quote name));
    4.97      fun reported_text () =
    4.98        if Context_Position.is_visible_generic context then
    4.99          maps (Token.reports_of_value o Token.closure) args1
   4.100 @@ -309,12 +326,11 @@
   4.101      (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
   4.102        (SOME x, (context', [])) => (Output.report (reported_text ()); (x, context'))
   4.103      | (_, (_, args2)) =>
   4.104 -        error ("Bad arguments for " ^ kind ^ " " ^ quote name ^ Position.here pos ^
   4.105 +        error ("Bad arguments for " ^ print_name () ^ Position.here pos ^
   4.106            (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
   4.107            Markup.markup_report (reported_text ())))
   4.108    end;
   4.109  
   4.110 -fun context_syntax kind scan src =
   4.111 -  apsnd Context.the_proof o syntax kind scan src o Context.Proof;
   4.112 +fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
   4.113  
   4.114  end;
     5.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 10 17:52:30 2014 +0100
     5.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 18:06:23 2014 +0100
     5.3 @@ -12,7 +12,6 @@
     5.4    val is_empty_binding: binding -> bool
     5.5    val print_attributes: Proof.context -> unit
     5.6    val check_name_generic: Context.generic -> xstring * Position.T -> string
     5.7 -  val check_src_generic: Context.generic -> src -> src
     5.8    val check_name: Proof.context -> xstring * Position.T -> string
     5.9    val check_src: Proof.context -> src -> src
    5.10    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    5.11 @@ -118,19 +117,15 @@
    5.12  (* check *)
    5.13  
    5.14  fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
    5.15 -fun check_src_generic context src = #1 (Args.check_src context (get_attributes context) src);
    5.16 +val check_name = check_name_generic o Context.Proof;
    5.17  
    5.18 -val check_name = check_name_generic o Context.Proof;
    5.19 -val check_src = check_src_generic o Context.Proof;
    5.20 +fun check_src ctxt src = #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src);
    5.21  
    5.22  
    5.23  (* pretty printing *)
    5.24  
    5.25 -fun pretty_attrib ctxt =
    5.26 -  Args.pretty_src (Name_Space.pretty ctxt (attribute_space ctxt)) ctxt;
    5.27 -
    5.28  fun pretty_attribs _ [] = []
    5.29 -  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (pretty_attrib ctxt) srcs)];
    5.30 +  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)];
    5.31  
    5.32  
    5.33  (* get attributes *)
    5.34 @@ -143,7 +138,7 @@
    5.35  val attribute_global = attribute_generic o Context.Theory;
    5.36  
    5.37  fun attribute_cmd ctxt = attribute ctxt o check_src ctxt;
    5.38 -fun attribute_cmd_global thy = attribute_global thy o check_src_generic (Context.Theory thy);
    5.39 +fun attribute_cmd_global thy = attribute_global thy o check_src (Proof_Context.init_global thy);
    5.40  
    5.41  
    5.42  (* attributed declarations *)
    5.43 @@ -174,11 +169,10 @@
    5.44  
    5.45  (* attribute setup *)
    5.46  
    5.47 -fun syntax scan = Args.syntax "attribute" scan;
    5.48 -
    5.49  fun setup name scan =
    5.50    add_attribute name
    5.51 -    (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
    5.52 +    (fn src => fn (ctxt, th) =>
    5.53 +      let val (a, ctxt') = Args.syntax_generic scan src ctxt in a (ctxt', th) end);
    5.54  
    5.55  fun attribute_setup name source cmt =
    5.56    Context.theory_map (ML_Context.expression (#pos source)
     6.1 --- a/src/Pure/Isar/method.ML	Mon Mar 10 17:52:30 2014 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Mon Mar 10 18:06:23 2014 +0100
     6.3 @@ -67,7 +67,6 @@
     6.4    val check_src: Proof.context -> src -> src
     6.5    val method: Proof.context -> src -> Proof.context -> method
     6.6    val method_cmd: Proof.context -> src -> Proof.context -> method
     6.7 -  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
     6.8    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
     6.9    val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    6.10    type modifier = (Proof.context -> Proof.context) * attribute
    6.11 @@ -340,7 +339,7 @@
    6.12  (* check *)
    6.13  
    6.14  fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
    6.15 -fun check_src ctxt src = #1 (Args.check_src (Context.Proof ctxt) (get_methods ctxt) src);
    6.16 +fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src);
    6.17  
    6.18  
    6.19  (* get methods *)
    6.20 @@ -354,11 +353,9 @@
    6.21  
    6.22  (* method setup *)
    6.23  
    6.24 -fun syntax scan = Args.context_syntax "method" scan;
    6.25 -
    6.26  fun setup name scan =
    6.27    add_method name
    6.28 -    (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
    6.29 +    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
    6.30  
    6.31  fun method_setup name source cmt =
    6.32    Context.theory_map (ML_Context.expression (#pos source)
     7.1 --- a/src/Pure/ML/ml_context.ML	Mon Mar 10 17:52:30 2014 +0100
     7.2 +++ b/src/Pure/ML/ml_context.ML	Mon Mar 10 18:06:23 2014 +0100
     7.3 @@ -115,8 +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 val (src', scan) = Args.check_src (Context.Proof ctxt) (get_antiqs ctxt) src
     7.8 -  in Args.context_syntax Markup.ML_antiquotationN scan src' ctxt end;
     7.9 +  let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src
    7.10 +  in Args.syntax scan src' ctxt end;
    7.11  
    7.12  
    7.13  (* parsing and evaluation *)
     8.1 --- a/src/Pure/Thy/term_style.ML	Mon Mar 10 17:52:30 2014 +0100
     8.2 +++ b/src/Pure/Thy/term_style.ML	Mon Mar 10 18:06:23 2014 +0100
     8.3 @@ -35,8 +35,8 @@
     8.4  fun parse_single ctxt =
     8.5    Parse.position Parse.xname -- Args.parse >> (fn (name, args) =>
     8.6      let
     8.7 -      val (src, parse) = Args.check_src (Context.Proof ctxt) (get_data ctxt) (Args.src name args);
     8.8 -      val (f, _) = Args.context_syntax "antiquotation_style" (Scan.lift parse) src ctxt;
     8.9 +      val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
    8.10 +      val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
    8.11      in f ctxt end);
    8.12  
    8.13  val parse = Args.context :|-- (fn ctxt => Scan.lift
     9.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 17:52:30 2014 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 18:06:23 2014 +0100
     9.3 @@ -92,7 +92,7 @@
     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 val (src', f) = Args.check_src (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) src
     9.8 +  let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src
     9.9    in f src' state ctxt end;
    9.10  
    9.11  fun option ((xname, pos), s) ctxt =
    9.12 @@ -115,7 +115,7 @@
    9.13  fun antiquotation name scan out =
    9.14    add_command name
    9.15      (fn src => fn state => fn ctxt =>
    9.16 -      let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
    9.17 +      let val (x, ctxt') = Args.syntax scan src ctxt
    9.18        in out {source = src, state = state, context = ctxt'} x end);
    9.19  
    9.20