src/Pure/Syntax/lexicon.ML

 (*  Title:      Pure/Syntax/lexicon.ML
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
-Scanner combinators and Isabelle's main lexer (used for terms and types).
+Scanner combinators and the main lexer (for terms and types).
 *)
 
 infix 5 -- ^^;
 infix 3 >>;
 infix 0 ||;
 
 signature SCANNER =
-  sig
+sig
   exception LEXICAL_ERROR
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
   val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c

   val empty_lexicon: lexicon
   val extend_lexicon: lexicon -> string list -> lexicon
   val make_lexicon: string list -> lexicon
   val merge_lexicons: lexicon -> lexicon -> lexicon
   val scan_literal: lexicon -> string list -> string * string list
-  end;
+end;
 
 signature LEXICON0 =
-  sig
+sig
   val is_identifier: string -> bool
+  val implode_xstr: string list -> string
+  val explode_xstr: string -> string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
   val scan_varname: string list -> indexname * string list
   val scan_var: string -> term
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
-  end;
+end;
 
 signature LEXICON =
-  sig
+sig
   include SCANNER
   include LEXICON0
   val is_xid: string -> bool
   val is_tid: string -> bool
   datatype token =

   val matching_tokens: token * token -> bool
   val token_assoc: (token option * 'a list) list * token -> 'a list
   val valued_token: token -> bool
   val predef_term: string -> token option
   val tokenize: lexicon -> bool -> string list -> token list
-  end;
+end;
 
 structure Lexicon : LEXICON =
 struct
+
 
 (** is_identifier etc. **)
 
 fun is_ident [] = false
   | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;

   | predef_term "tid" = Some (TFreeSy "tid")
   | predef_term "tvar" = Some (TVarSy "tvar")
   | predef_term "xnum" = Some (NumSy "xnum")
   | predef_term "xstr" = Some (StrSy "xstr")
   | predef_term _ = None;
+
+
+(*  xstr tokens *)
+
+fun implode_xstr cs = enclose "''" "''" (implode cs);
+
+fun explode_xstr str =
+  rev (tl (tl (rev (tl (tl (explode str))))));
 
 
 
 (** datatype lexicon **)
 

           let
             val (cs', cs'') = scan_str cs handle ERROR =>
               error ("Lexical error: missing quotes at end of string " ^
                 quote (implode chs));
           in
-            scan (StrSy (implode cs') :: rev_toks, cs'')
+            scan (StrSy (implode_xstr cs') :: rev_toks, cs'')
           end
       | scan (rev_toks, chs as c :: cs) =
           if is_blank c then scan (rev_toks, cs)
           else
             (case max_of scan_lit scan_val chs of

       scan_rest >> (free o implode);
   in
     #1 (scan (explode str))
   end;
 
+
 end;
-