tuned message -- more markup;
authorwenzelm
Tue Feb 25 17:23:20 2014 +0100 (2014-02-25)
changeset 55745b865c3035d5c
parent 55744 4a4e5686e091
child 55746 97f390fa0f3a
tuned message -- more markup;
src/Pure/Isar/args.ML
src/Pure/Isar/token.ML
     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  
     2.1 --- a/src/Pure/Isar/token.ML	Tue Feb 25 17:03:55 2014 +0100
     2.2 +++ b/src/Pure/Isar/token.ML	Tue Feb 25 17:23:20 2014 +0100
     2.3 @@ -44,6 +44,7 @@
     2.4    val content_of: T -> string
     2.5    val markup: T -> Markup.T * string
     2.6    val unparse: T -> string
     2.7 +  val print: T -> string
     2.8    val text_of: T -> string * string
     2.9    val get_files: T -> file Exn.result list
    2.10    val put_files: file Exn.result list -> T -> T
    2.11 @@ -263,6 +264,8 @@
    2.12    | EOF => ""
    2.13    | _ => x);
    2.14  
    2.15 +fun print tok = Markup.markup (#1 (markup tok)) (unparse tok);
    2.16 +
    2.17  fun text_of tok =
    2.18    if is_semicolon tok then ("terminator", "")
    2.19    else