# HG changeset patch
# User wenzelm
# Date 1165510734 -3600
# Node ID 9300bec44e6a8c726c4e2966684aff62db9f3d3f
# Parent  627c90b310c1714a7652ce8bc7b656468ac45159
added input_mode;

diff -r 627c90b310c1 -r 9300bec44e6a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Dec 07 17:58:52 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Dec 07 17:58:54 2006 +0100
@@ -39,6 +39,7 @@
   val is_keyword: syntax -> string -> bool
   type mode
   val default_mode: mode
+  val input_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
@@ -185,6 +186,7 @@
 
 type mode = string * bool;
 val default_mode = ("", true);
+val input_mode = ("input", true);
 
 
 (* empty_syntax *)