src/Pure/Syntax/lexicon.ML
changeset 5868 0022d0a913b5
parent 5860 ed11c9890852
child 6962 399643633529
equal deleted inserted replaced
5867:1c4806b4bf43 5868:0022d0a913b5
   239 
   239 
   240 
   240 
   241 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
   241 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
   242 
   242 
   243 fun explode_xstr str =
   243 fun explode_xstr str =
   244   #1 (Scan.error (Scan.finite Symbol.stopper scan_str) (Symbol.explode str));
   244   (case Scan.read Symbol.stopper scan_str (Symbol.explode str) of
       
   245     Some cs => cs
       
   246   | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
   245 
   247 
   246 
   248 
   247 
   249 
   248 (** tokenize **)
   250 (** tokenize **)
   249 
   251 
   255 
   257 
   256     val scan_val =
   258     val scan_val =
   257       scan_tvar >> pair TVarSy ||
   259       scan_tvar >> pair TVarSy ||
   258       scan_var >> pair VarSy ||
   260       scan_var >> pair VarSy ||
   259       scan_tid >> pair TFreeSy ||
   261       scan_tid >> pair TFreeSy ||
   260       $$ "#" ^^ scan_int >> pair NumSy ||		(* FIXME remove "#" *)
   262       $$ "#" ^^ scan_int >> pair NumSy ||
   261       scan_longid >> pair LongIdentSy ||
   263       scan_longid >> pair LongIdentSy ||
   262       scan_xid >> pair IdentSy;
   264       scan_xid >> pair IdentSy;
   263 
   265 
   264     val scan_lit = Scan.literal lex >> (pair Token o implode);
   266     val scan_lit = Scan.literal lex >> (pair Token o implode);
   265 
   267 
   300 
   302 
   301 
   303 
   302 (* indexname *)
   304 (* indexname *)
   303 
   305 
   304 fun indexname cs =
   306 fun indexname cs =
   305   (case Scan.error (Scan.finite Symbol.stopper (Scan.option scan_vname)) cs of
   307   (case Scan.read Symbol.stopper scan_vname cs of
   306     (Some xi, []) => xi
   308     Some xi => xi
   307   | _ => error ("Lexical error in variable name: " ^ quote (implode cs)));
   309   | _ => error ("Lexical error in variable name: " ^ quote (implode cs)));
   308 
   310 
   309 
   311 
   310 (* read_var *)
   312 (* read_var *)
   311 
   313 
   319 
   321 
   320     val scan =
   322     val scan =
   321       $$ "?" |-- $$ "'" |-- scan_vname >> tvar ||
   323       $$ "?" |-- $$ "'" |-- scan_vname >> tvar ||
   322       $$ "?" |-- scan_vname >> var ||
   324       $$ "?" |-- scan_vname >> var ||
   323       Scan.any Symbol.not_eof >> (free o implode);
   325       Scan.any Symbol.not_eof >> (free o implode);
   324   in
   326   in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
   325     #1 (Scan.error (Scan.finite Symbol.stopper scan) (Symbol.explode str))
       
   326   end;
       
   327 
   327 
   328 
   328 
   329 (* variable kinds *)
   329 (* variable kinds *)
   330 
   330 
   331 val binding = suffix "_BIND_";
   331 val binding = suffix "_BIND_";
   336 
   336 
   337 
   337 
   338 (* read_nat *)
   338 (* read_nat *)
   339 
   339 
   340 fun read_nat str =
   340 fun read_nat str =
   341   (case Scan.finite Symbol.stopper (Scan.option scan_digits1) (Symbol.explode str) of
   341   apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
   342     (Some cs, []) => Some (#1 (Term.read_int cs))
       
   343   | _ => None);
       
   344 
   342 
   345 
   343 
   346 end;
   344 end;