src/Pure/Syntax/syntax.ML

   val eq_syntax: syntax * syntax -> bool
   val is_keyword: syntax -> string -> bool
   type mode
   val default_mode: mode
   val input_mode: mode
+  val internal_mode: mode
   val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
   val extend_const_gram: (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val extend_consts: string list -> syntax -> syntax
   val extend_trfuns:

 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 
 type mode = string * bool;
 val default_mode = ("", true);
 val input_mode = ("input", true);
+val internal_mode = ("internal", true);
 
 
 (* empty_syntax *)
 
 val empty_syntax = Syntax