--- a/src/Pure/Isar/token.ML Tue Aug 09 14:41:27 2016 +0200
+++ b/src/Pure/Isar/token.ML Tue Aug 09 19:44:28 2016 +0200
@@ -91,6 +91,7 @@
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
val read_cartouche: Symbol_Pos.T list -> T
val explode: Keyword.keywords -> Position.T -> string -> T list
+ val print_name: Keyword.keywords -> string -> string
val make: (int * int) * string -> Position.T -> T * Position.T
val make_string: string * Position.T -> T
val make_int: int -> T list
@@ -655,6 +656,14 @@
Source.exhaust;
+(* print name in parsable form *)
+
+fun print_name keywords name =
+ ((case explode keywords Position.none name of
+ [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok))
+ | _ => true) ? Symbol_Pos.quote_string_qq) name;
+
+
(* make *)
fun make ((k, n), s) pos =