1.1 --- a/src/Tools/Code/code_target.ML	Mon May 17 15:05:32 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon May 17 15:11:25 2010 +0200
     1.3 @@ -19,14 +19,13 @@
     1.4  
     1.5    type destination
     1.6    type serialization
     1.7 -  val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
     1.8 -    -> OuterLex.token list -> 'a
     1.9 +  val parse_args: 'a parser -> Token.T list -> 'a
    1.10    val stmt_names_of_destination: destination -> string list
    1.11    val mk_serialization: string -> ('a -> unit) option
    1.12      -> (Path.T option -> 'a -> unit)
    1.13      -> ('a -> string * string option list)
    1.14      -> 'a -> serialization
    1.15 -  val serialize: theory -> string -> int option -> string option -> OuterLex.token list
    1.16 +  val serialize: theory -> string -> int option -> string option -> Token.T list
    1.17      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.18    val serialize_custom: theory -> string * (serializer * literals)
    1.19      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.20 @@ -105,7 +104,7 @@
    1.21  
    1.22  type serializer =
    1.23    string option                         (*module name*)
    1.24 -  -> OuterLex.token list                (*arguments*)
    1.25 +  -> Token.T list                       (*arguments*)
    1.26    -> (string -> string)                 (*labelled_name*)
    1.27    -> string list                        (*reserved symbols*)
    1.28    -> (string * Pretty.T) list           (*includes*)
    1.29 @@ -498,7 +497,7 @@
    1.30  val allow_abort_cmd = gen_allow_abort Code.read_const;
    1.31  
    1.32  fun parse_args f args =
    1.33 -  case Scan.read OuterLex.stopper f args
    1.34 +  case Scan.read Token.stopper f args
    1.35     of SOME x => x
    1.36      | NONE => error "Bad serializer arguments";
    1.37  
    1.38 @@ -575,8 +574,8 @@
    1.39      K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
    1.40  
    1.41  fun shell_command thyname cmd = Toplevel.program (fn _ =>
    1.42 -  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
    1.43 -    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
    1.44 +  (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
    1.45 +    ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
    1.46     of SOME f => (writeln "Now generating code..."; f (theory thyname))
    1.47      | NONE => error ("Bad directive " ^ quote cmd)))
    1.48    handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;