src/Pure/Isar/token.ML

--- 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 =