src/Pure/Isar/args.ML
changeset 55745 b865c3035d5c
parent 55708 f4b114070675
child 55828 42ac3cfb89f6
     1.1 --- a/src/Pure/Isar/args.ML	Tue Feb 25 17:03:55 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Feb 25 17:23:20 2014 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4        | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
     1.5        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
     1.6        | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
     1.7 -      | _ => Pretty.str (Token.unparse arg));
     1.8 +      | _ => Pretty.mark_str (#1 (Token.markup arg), Token.unparse arg));
     1.9      val (s, args) = #1 (dest_src src);
    1.10    in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
    1.11  
    1.12 @@ -291,8 +291,8 @@
    1.13    (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
    1.14      (SOME x, (st', [])) => (x, st')
    1.15    | (_, (_, args')) =>
    1.16 -      error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments" ^
    1.17 -        (if null args' then "" else "\n  " ^ space_implode " " (map Token.unparse args'))));
    1.18 +      error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
    1.19 +        (if null args' then "" else ":\n  " ^ space_implode " " (map Token.print args'))));
    1.20  
    1.21  fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
    1.22