src/Pure/Syntax/lexicon.ML

 Lexer for the inner Isabelle syntax (terms and types).
 *)
 
 signature LEXICON =
 sig
+  structure Syntax:
+  sig
+    val const: string -> term
+    val free: string -> term
+    val var: indexname -> term
+  end
   val is_identifier: string -> bool
   val is_ascii_identifier: string -> bool
   val is_xid: string -> bool
   val is_tid: string -> bool
   val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list

   val predef_term: string -> token option
   val implode_xstr: string list -> string
   val explode_xstr: string -> string list
   val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
   val read_indexname: string -> indexname
-  val const: string -> term
-  val free: string -> term
-  val var: indexname -> term
   val read_var: string -> term
   val read_variable: string -> indexname option
   val read_nat: string -> int option
   val read_int: string -> int option
   val read_xnum: string -> {radix: int, leading_zeros: int, value: int}

 end;
 
 structure Lexicon: LEXICON =
 struct
 
+(** syntaxtic terms **)
+
+structure Syntax =
+struct
+
+fun const c = Const (c, dummyT);
+fun free x = Free (x, dummyT);
+fun var xi = Var (xi, dummyT);
+
+end;
+
+
+
 (** is_identifier etc. **)
 
 val is_identifier = Symbol.is_ident o Symbol.explode;
 
 fun is_ascii_identifier s =

   | _ => error ("Lexical error in variable name: " ^ quote s));
 
 
 (* read_var *)
 
-fun const c = Const (c, dummyT);
-fun free x = Free (x, dummyT);
-fun var xi = Var (xi, dummyT);
-
 fun read_var str =
   let
     val scan =
-      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
-      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
+      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
+        >> Syntax.var ||
+      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
+        >> (Syntax.free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
 
 
 (* read_variable *)
 

 
 val is_marked =
   unmark {case_class = K true, case_type = K true, case_const = K true,
     case_fixed = K true, case_default = K false};
 
-val dummy_type = const (mark_type "dummy");
-val fun_type = const (mark_type "fun");
-
-end;
+val dummy_type = Syntax.const (mark_type "dummy");
+val fun_type = Syntax.const (mark_type "fun");
+
+end;