tuned;
authorwenzelm
Mon Mar 10 22:08:51 2014 +0100 (2014-03-10)
changeset 560377b716baac02c
parent 56036 6c3fc3b5592a
child 56038 0e2dec666152
tuned;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 21:58:54 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 22:08:51 2014 +0100
     1.3 @@ -84,11 +84,7 @@
     1.4  
     1.5  fun src name args = Src {name = name, args = args, output_info = NONE};
     1.6  
     1.7 -fun map_args f (Src {name, args, output_info}) =
     1.8 -  Src {name = name, args = map f args, output_info = output_info};
     1.9 -
    1.10  fun name_of_src (Src {name, ...}) = name;
    1.11 -fun args_of_src (Src {args, ...}) = args;
    1.12  
    1.13  fun range_of_src (Src {name = (_, pos), args, ...}) =
    1.14    if null args then pos
    1.15 @@ -96,15 +92,15 @@
    1.16  
    1.17  fun unparse_src (Src {args, ...}) = map Token.unparse args;
    1.18  
    1.19 -fun pretty_name (Src {name = (name, _), output_info, ...}) =
    1.20 -  (case output_info of
    1.21 -    NONE => Pretty.str name
    1.22 -  | SOME (_, markup) => Pretty.mark_str (markup, name));
    1.23 -
    1.24  fun pretty_src ctxt src =
    1.25    let
    1.26 +    val Src {name = (name, _), args, output_info} = src;
    1.27 +    val prt_name =
    1.28 +      (case output_info of
    1.29 +        NONE => Pretty.str name
    1.30 +      | SOME (_, markup) => Pretty.mark_str (markup, name));
    1.31      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    1.32 -    fun prt arg =
    1.33 +    fun prt_arg arg =
    1.34        (case Token.get_value arg of
    1.35          SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup v, s)
    1.36        | SOME (Token.Text s) => Pretty.str (quote s)
    1.37 @@ -112,7 +108,7 @@
    1.38        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    1.39        | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    1.40        | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    1.41 -  in Pretty.block (Pretty.breaks (pretty_name src :: map prt (args_of_src src))) end;
    1.42 +  in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
    1.43  
    1.44  
    1.45  (* check *)
    1.46 @@ -128,6 +124,9 @@
    1.47  
    1.48  (* values *)
    1.49  
    1.50 +fun map_args f (Src {name, args, output_info}) =
    1.51 +  Src {name = name, args = map f args, output_info = output_info};
    1.52 +
    1.53  fun transform_values phi = map_args (Token.map_value
    1.54    (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
    1.55      | Token.Term t => Token.Term (Morphism.term phi t)
    1.56 @@ -316,10 +315,6 @@
    1.57  fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
    1.58    let
    1.59      val args1 = map Token.init_assignable args0;
    1.60 -    fun print_name () =
    1.61 -      (case output_info of
    1.62 -        NONE => quote name
    1.63 -      | SOME (kind, markup) => kind ^ " " ^ Markup.markup markup (quote name));
    1.64      fun reported_text () =
    1.65        if Context_Position.is_visible_generic context then
    1.66          maps (Token.reports_of_value o Token.closure) args1
    1.67 @@ -328,11 +323,21 @@
    1.68        else "";
    1.69    in
    1.70      (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
    1.71 -      (SOME x, (context', [])) => (Output.report (reported_text ()); (x, context'))
    1.72 +      (SOME x, (context', [])) =>
    1.73 +        let val _ = Output.report (reported_text ())
    1.74 +        in (x, context') end
    1.75      | (_, (_, args2)) =>
    1.76 -        error ("Bad arguments for " ^ print_name () ^ Position.here pos ^
    1.77 -          (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
    1.78 -          Markup.markup_report (reported_text ())))
    1.79 +        let
    1.80 +          val print_name =
    1.81 +            (case output_info of
    1.82 +              NONE => quote name
    1.83 +            | SOME (kind, markup) => kind ^ " " ^ quote (Markup.markup markup name));
    1.84 +          val print_args =
    1.85 +            if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2);
    1.86 +        in
    1.87 +          error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
    1.88 +            Markup.markup_report (reported_text ()))
    1.89 +        end)
    1.90    end;
    1.91  
    1.92  fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;