renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
authorwenzelm
Mon May 17 15:11:25 2010 +0200 (2010-05-17)
changeset 36959f5417836dbea
parent 36958 ad5313f1bd30
child 36960 01594f816e3a
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;
NEWS
src/HOL/Import/import_syntax.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/Pure/IsaMakefile
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_context.ML
src/Pure/ROOT.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/NEWS	Mon May 17 15:05:32 2010 +0200
     1.2 +++ b/NEWS	Mon May 17 15:11:25 2010 +0200
     1.3 @@ -505,9 +505,10 @@
     1.4  * Renamed some important ML structures, while keeping the old names as
     1.5  legacy aliases for some time:
     1.6  
     1.7 +  OuterKeyword  ~>  Keyword
     1.8 +  OuterLex      ~>  Token
     1.9 +  OuterParse    ~>  Parse
    1.10    OuterSyntax   ~>  Outer_Syntax
    1.11 -  OuterKeyword  ~>  Keyword
    1.12 -  OuterParse    ~>  Parse
    1.13    SpecParse     ~>  Parse_Spec
    1.14  
    1.15  
     2.1 --- a/src/HOL/Import/import_syntax.ML	Mon May 17 15:05:32 2010 +0200
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Mon May 17 15:11:25 2010 +0200
     2.3 @@ -4,26 +4,23 @@
     2.4  
     2.5  signature HOL4_IMPORT_SYNTAX =
     2.6  sig
     2.7 -    type token = OuterLex.token
     2.8 -    type command  = token list -> (theory -> theory) * token list 
     2.9 -
    2.10 -    val import_segment: token list -> (theory -> theory) * token list
    2.11 -    val import_theory : token list -> (theory -> theory) * token list
    2.12 -    val end_import    : token list -> (theory -> theory) * token list
    2.13 -
    2.14 -    val setup_theory  : token list -> (theory -> theory) * token list
    2.15 -    val end_setup     : token list -> (theory -> theory) * token list
    2.16 +    val import_segment: (theory -> theory) parser
    2.17 +    val import_theory : (theory -> theory) parser
    2.18 +    val end_import    : (theory -> theory) parser
    2.19 +                        
    2.20 +    val setup_theory  : (theory -> theory) parser
    2.21 +    val end_setup     : (theory -> theory) parser
    2.22 +                        
    2.23 +    val thm_maps      : (theory -> theory) parser
    2.24 +    val ignore_thms   : (theory -> theory) parser
    2.25 +    val type_maps     : (theory -> theory) parser
    2.26 +    val def_maps      : (theory -> theory) parser
    2.27 +    val const_maps    : (theory -> theory) parser
    2.28 +    val const_moves   : (theory -> theory) parser
    2.29 +    val const_renames : (theory -> theory) parser
    2.30  
    2.31 -    val thm_maps      : token list -> (theory -> theory) * token list
    2.32 -    val ignore_thms   : token list -> (theory -> theory) * token list
    2.33 -    val type_maps     : token list -> (theory -> theory) * token list
    2.34 -    val def_maps      : token list -> (theory -> theory) * token list
    2.35 -    val const_maps    : token list -> (theory -> theory) * token list
    2.36 -    val const_moves   : token list -> (theory -> theory) * token list
    2.37 -    val const_renames : token list -> (theory -> theory) * token list
    2.38 -
    2.39 -    val skip_import_dir : token list -> (theory -> theory) * token list
    2.40 -    val skip_import     : token list -> (theory -> theory) * token list
    2.41 +    val skip_import_dir : (theory -> theory) parser
    2.42 +    val skip_import     : (theory -> theory) parser
    2.43  
    2.44      val setup        : unit -> unit
    2.45  end
    2.46 @@ -31,9 +28,6 @@
    2.47  structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
    2.48  struct
    2.49  
    2.50 -type token = OuterLex.token
    2.51 -type command  = token list -> (theory -> theory) * token list 
    2.52 -
    2.53  local structure P = OuterParse and K = OuterKeyword in
    2.54  
    2.55  (* Parsers *)
    2.56 @@ -48,11 +42,11 @@
    2.57                                        |> add_dump (";setup_theory " ^ thyname))
    2.58  
    2.59  fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
    2.60 -val skip_import_dir : command = P.string >> do_skip_import_dir
    2.61 +val skip_import_dir = P.string >> do_skip_import_dir
    2.62  
    2.63  val lower = String.map Char.toLower
    2.64  fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
    2.65 -val skip_import : command = P.short_ident >> do_skip_import
    2.66 +val skip_import = P.short_ident >> do_skip_import
    2.67  
    2.68  fun end_import toks =
    2.69      Scan.succeed
    2.70 @@ -160,8 +154,8 @@
    2.71            (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
    2.72                    Scan.empty_lexicon)
    2.73          val get_lexes = fn () => !lexes
    2.74 -        val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
    2.75 -        val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
    2.76 +        val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
    2.77 +        val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
    2.78          val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
    2.79          val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
    2.80          val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 15:05:32 2010 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 17 15:11:25 2010 +0200
     3.3 @@ -335,9 +335,9 @@
     3.4    in
     3.5      Source.of_string name
     3.6      |> Symbol.source {do_recover=false}
     3.7 -    |> OuterLex.source {do_recover=SOME false} lex Position.start
     3.8 -    |> OuterLex.source_proper
     3.9 -    |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
    3.10 +    |> Token.source {do_recover=SOME false} lex Position.start
    3.11 +    |> Token.source_proper
    3.12 +    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    3.13      |> Source.exhaust
    3.14    end
    3.15  
     4.1 --- a/src/Pure/IsaMakefile	Mon May 17 15:05:32 2010 +0200
     4.2 +++ b/src/Pure/IsaMakefile	Mon May 17 15:11:25 2010 +0200
     4.3 @@ -67,24 +67,25 @@
     4.4    Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
     4.5    Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
     4.6    Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
     4.7 -  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML	\
     4.8 +  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
     4.9    Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
    4.10    Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
    4.11    Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
    4.12    Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
    4.13    Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML		\
    4.14 -  Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
    4.15 -  ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
    4.16 -  ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
    4.17 -  ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
    4.18 -  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
    4.19 -  Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
    4.20 -  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
    4.21 -  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
    4.22 -  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
    4.23 -  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
    4.24 -  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
    4.25 -  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
    4.26 +  Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML			\
    4.27 +  Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML			\
    4.28 +  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
    4.29 +  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
    4.30 +  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
    4.31 +  ML-Systems/use_context.ML Proof/extraction.ML				\
    4.32 +  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    4.33 +  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
    4.34 +  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
    4.35 +  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
    4.36 +  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
    4.37 +  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
    4.38 +  ProofGeneral/proof_general_emacs.ML					\
    4.39    ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
    4.40    Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
    4.41    Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
     5.1 --- a/src/Pure/Isar/args.ML	Mon May 17 15:05:32 2010 +0200
     5.2 +++ b/src/Pure/Isar/args.ML	Mon May 17 15:11:25 2010 +0200
     5.3 @@ -7,10 +7,9 @@
     5.4  
     5.5  signature ARGS =
     5.6  sig
     5.7 -  type token = OuterLex.token
     5.8    type src
     5.9 -  val src: (string * token list) * Position.T -> src
    5.10 -  val dest_src: src -> (string * token list) * Position.T
    5.11 +  val src: (string * Token.T list) * Position.T -> src
    5.12 +  val dest_src: src -> (string * Token.T list) * Position.T
    5.13    val pretty_src: Proof.context -> src -> Pretty.T
    5.14    val map_name: (string -> string) -> src -> src
    5.15    val morph_values: morphism -> src -> src
    5.16 @@ -57,8 +56,8 @@
    5.17    val const: bool -> string context_parser
    5.18    val const_proper: bool -> string context_parser
    5.19    val goal_spec: ((int -> tactic) -> tactic) context_parser
    5.20 -  val parse: token list parser
    5.21 -  val parse1: (string -> bool) -> token list parser
    5.22 +  val parse: Token.T list parser
    5.23 +  val parse1: (string -> bool) -> Token.T list parser
    5.24    val attribs: (string -> string) -> src list parser
    5.25    val opt_attribs: (string -> string) -> src list parser
    5.26    val thm_name: (string -> string) -> string -> (binding * src list) parser
    5.27 @@ -70,15 +69,9 @@
    5.28  structure Args: ARGS =
    5.29  struct
    5.30  
    5.31 -structure T = OuterLex;
    5.32 -
    5.33 -type token = T.token;
    5.34 -
    5.35 -
    5.36 -
    5.37  (** datatype src **)
    5.38  
    5.39 -datatype src = Src of (string * token list) * Position.T;
    5.40 +datatype src = Src of (string * Token.T list) * Position.T;
    5.41  
    5.42  val src = Src;
    5.43  fun dest_src (Src src) = src;
    5.44 @@ -87,12 +80,12 @@
    5.45    let
    5.46      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    5.47      fun prt arg =
    5.48 -      (case T.get_value arg of
    5.49 -        SOME (T.Text s) => Pretty.str (quote s)
    5.50 -      | SOME (T.Typ T) => Syntax.pretty_typ ctxt T
    5.51 -      | SOME (T.Term t) => Syntax.pretty_term ctxt t
    5.52 -      | SOME (T.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    5.53 -      | _ => Pretty.str (T.unparse arg));
    5.54 +      (case Token.get_value arg of
    5.55 +        SOME (Token.Text s) => Pretty.str (quote s)
    5.56 +      | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
    5.57 +      | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    5.58 +      | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    5.59 +      | _ => Pretty.str (Token.unparse arg));
    5.60      val (s, args) = #1 (dest_src src);
    5.61    in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
    5.62  
    5.63 @@ -102,15 +95,15 @@
    5.64  
    5.65  (* values *)
    5.66  
    5.67 -fun morph_values phi = map_args (T.map_value
    5.68 -  (fn T.Text s => T.Text s
    5.69 -    | T.Typ T => T.Typ (Morphism.typ phi T)
    5.70 -    | T.Term t => T.Term (Morphism.term phi t)
    5.71 -    | T.Fact ths => T.Fact (Morphism.fact phi ths)
    5.72 -    | T.Attribute att => T.Attribute (Morphism.transform phi att)));
    5.73 +fun morph_values phi = map_args (Token.map_value
    5.74 +  (fn Token.Text s => Token.Text s
    5.75 +    | Token.Typ T => Token.Typ (Morphism.typ phi T)
    5.76 +    | Token.Term t => Token.Term (Morphism.term phi t)
    5.77 +    | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
    5.78 +    | Token.Attribute att => Token.Attribute (Morphism.transform phi att)));
    5.79  
    5.80 -val assignable = map_args T.assignable;
    5.81 -val closure = map_args T.closure;
    5.82 +val assignable = map_args Token.assignable;
    5.83 +val closure = map_args Token.closure;
    5.84  
    5.85  
    5.86  
    5.87 @@ -134,7 +127,7 @@
    5.88  val alt_string = token Parse.alt_string;
    5.89  val symbolic = token Parse.keyword_ident_or_symbolic;
    5.90  
    5.91 -fun $$$ x = (ident >> T.content_of || Parse.keyword)
    5.92 +fun $$$ x = (ident >> Token.content_of || Parse.keyword)
    5.93    :|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
    5.94  
    5.95  
    5.96 @@ -153,39 +146,40 @@
    5.97  fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
    5.98  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
    5.99  
   5.100 -val name_source = named >> T.source_of;
   5.101 -val name_source_position = named >> T.source_position_of;
   5.102 +val name_source = named >> Token.source_of;
   5.103 +val name_source_position = named >> Token.source_position_of;
   5.104  
   5.105 -val name = named >> T.content_of;
   5.106 +val name = named >> Token.content_of;
   5.107  val binding = Parse.position name >> Binding.make;
   5.108 -val alt_name = alt_string >> T.content_of;
   5.109 -val symbol = symbolic >> T.content_of;
   5.110 +val alt_name = alt_string >> Token.content_of;
   5.111 +val symbol = symbolic >> Token.content_of;
   5.112  val liberal_name = symbol || name;
   5.113  
   5.114 -val var = (ident >> T.content_of) :|-- (fn x =>
   5.115 +val var = (ident >> Token.content_of) :|-- (fn x =>
   5.116    (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
   5.117  
   5.118  
   5.119  (* values *)
   5.120  
   5.121  fun value dest = Scan.some (fn arg =>
   5.122 -  (case T.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
   5.123 +  (case Token.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
   5.124  
   5.125  fun evaluate mk eval arg =
   5.126 -  let val x = eval arg in (T.assign (SOME (mk x)) arg; x) end;
   5.127 +  let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
   5.128 +
   5.129 +val internal_text = value (fn Token.Text s => s);
   5.130 +val internal_typ = value (fn Token.Typ T => T);
   5.131 +val internal_term = value (fn Token.Term t => t);
   5.132 +val internal_fact = value (fn Token.Fact ths => ths);
   5.133 +val internal_attribute = value (fn Token.Attribute att => att);
   5.134  
   5.135 -val internal_text = value (fn T.Text s => s);
   5.136 -val internal_typ = value (fn T.Typ T => T);
   5.137 -val internal_term = value (fn T.Term t => t);
   5.138 -val internal_fact = value (fn T.Fact ths => ths);
   5.139 -val internal_attribute = value (fn T.Attribute att => att);
   5.140 -
   5.141 -fun named_text intern = internal_text || named >> evaluate T.Text (intern o T.content_of);
   5.142 -fun named_typ readT = internal_typ || named >> evaluate T.Typ (readT o T.source_of);
   5.143 -fun named_term read = internal_term || named >> evaluate T.Term (read o T.source_of);
   5.144 -fun named_fact get = internal_fact || named >> evaluate T.Fact (get o T.content_of) ||
   5.145 -  alt_string >> evaluate T.Fact (get o T.source_of);
   5.146 -fun named_attribute att = internal_attribute || named >> evaluate T.Attribute (att o T.content_of);
   5.147 +fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
   5.148 +fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
   5.149 +fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
   5.150 +fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
   5.151 +  alt_string >> evaluate Token.Fact (get o Token.source_of);
   5.152 +fun named_attribute att =
   5.153 +  internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
   5.154  
   5.155  
   5.156  (* terms and types *)
   5.157 @@ -243,7 +237,7 @@
   5.158        (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
   5.159    in (args, args1) end;
   5.160  
   5.161 -val parse = #1 (parse_args T.ident_or_symbolic) false;
   5.162 +val parse = #1 (parse_args Token.ident_or_symbolic) false;
   5.163  fun parse1 is_symid = #2 (parse_args is_symid) false;
   5.164  
   5.165  
   5.166 @@ -252,7 +246,7 @@
   5.167  fun attribs intern =
   5.168    let
   5.169      val attrib_name = internal_text || (symbolic || named)
   5.170 -      >> evaluate T.Text (intern o T.content_of);
   5.171 +      >> evaluate Token.Text (intern o Token.content_of);
   5.172      val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
   5.173    in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
   5.174  
   5.175 @@ -273,11 +267,11 @@
   5.176  (** syntax wrapper **)
   5.177  
   5.178  fun syntax kind scan (Src ((s, args), pos)) st =
   5.179 -  (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
   5.180 +  (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
   5.181      (SOME x, (st', [])) => (x, st')
   5.182    | (_, (_, args')) =>
   5.183        error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
   5.184 -        space_implode " " (map T.unparse args')));
   5.185 +        space_implode " " (map Token.unparse args')));
   5.186  
   5.187  fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
   5.188  
     6.1 --- a/src/Pure/Isar/attrib.ML	Mon May 17 15:05:32 2010 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Mon May 17 15:11:25 2010 +0200
     6.3 @@ -47,9 +47,6 @@
     6.4  structure Attrib: ATTRIB =
     6.5  struct
     6.6  
     6.7 -structure T = OuterLex;
     6.8 -
     6.9 -
    6.10  (* source and bindings *)
    6.11  
    6.12  type src = Args.src;
    6.13 @@ -216,7 +213,7 @@
    6.14  
    6.15  (* internal *)
    6.16  
    6.17 -fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
    6.18 +fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
    6.19  
    6.20  
    6.21  (* rule composition *)
     7.1 --- a/src/Pure/Isar/method.ML	Mon May 17 15:05:32 2010 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Mon May 17 15:11:25 2010 +0200
     7.3 @@ -411,7 +411,7 @@
     7.4  (* outer parser *)
     7.5  
     7.6  fun is_symid_meth s =
     7.7 -  s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s;
     7.8 +  s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
     7.9  
    7.10  local
    7.11  
     8.1 --- a/src/Pure/Isar/outer_lex.ML	Mon May 17 15:05:32 2010 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,390 +0,0 @@
     8.4 -(*  Title:      Pure/Isar/outer_lex.ML
     8.5 -    Author:     Markus Wenzel, TU Muenchen
     8.6 -
     8.7 -Outer lexical syntax for Isabelle/Isar.
     8.8 -*)
     8.9 -
    8.10 -signature OUTER_LEX =
    8.11 -sig
    8.12 -  datatype token_kind =
    8.13 -    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    8.14 -    Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
    8.15 -    Malformed | Error of string | Sync | EOF
    8.16 -  datatype value =
    8.17 -    Text of string | Typ of typ | Term of term | Fact of thm list |
    8.18 -    Attribute of morphism -> attribute
    8.19 -  type token
    8.20 -  val str_of_kind: token_kind -> string
    8.21 -  val position_of: token -> Position.T
    8.22 -  val end_position_of: token -> Position.T
    8.23 -  val pos_of: token -> string
    8.24 -  val eof: token
    8.25 -  val is_eof: token -> bool
    8.26 -  val not_eof: token -> bool
    8.27 -  val not_sync: token -> bool
    8.28 -  val stopper: token Scan.stopper
    8.29 -  val kind_of: token -> token_kind
    8.30 -  val is_kind: token_kind -> token -> bool
    8.31 -  val keyword_with: (string -> bool) -> token -> bool
    8.32 -  val ident_with: (string -> bool) -> token -> bool
    8.33 -  val is_proper: token -> bool
    8.34 -  val is_semicolon: token -> bool
    8.35 -  val is_comment: token -> bool
    8.36 -  val is_begin_ignore: token -> bool
    8.37 -  val is_end_ignore: token -> bool
    8.38 -  val is_blank: token -> bool
    8.39 -  val is_newline: token -> bool
    8.40 -  val source_of: token -> string
    8.41 -  val source_position_of: token -> Symbol_Pos.text * Position.T
    8.42 -  val content_of: token -> string
    8.43 -  val unparse: token -> string
    8.44 -  val text_of: token -> string * string
    8.45 -  val get_value: token -> value option
    8.46 -  val map_value: (value -> value) -> token -> token
    8.47 -  val mk_text: string -> token
    8.48 -  val mk_typ: typ -> token
    8.49 -  val mk_term: term -> token
    8.50 -  val mk_fact: thm list -> token
    8.51 -  val mk_attribute: (morphism -> attribute) -> token
    8.52 -  val assignable: token -> token
    8.53 -  val assign: value option -> token -> unit
    8.54 -  val closure: token -> token
    8.55 -  val ident_or_symbolic: string -> bool
    8.56 -  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
    8.57 -  val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
    8.58 -  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    8.59 -    (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
    8.60 -  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    8.61 -    Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
    8.62 -      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
    8.63 -  val read_antiq: Scan.lexicon -> (token list -> 'a * token list) ->
    8.64 -    Symbol_Pos.T list * Position.T -> 'a
    8.65 -end;
    8.66 -
    8.67 -structure OuterLex: OUTER_LEX =
    8.68 -struct
    8.69 -
    8.70 -(** tokens **)
    8.71 -
    8.72 -(* token values *)
    8.73 -
    8.74 -(*The value slot assigns an (optional) internal value to a token,
    8.75 -  usually as a side-effect of special scanner setup (see also
    8.76 -  args.ML).  Note that an assignable ref designates an intermediate
    8.77 -  state of internalization -- it is NOT meant to persist.*)
    8.78 -
    8.79 -datatype value =
    8.80 -  Text of string |
    8.81 -  Typ of typ |
    8.82 -  Term of term |
    8.83 -  Fact of thm list |
    8.84 -  Attribute of morphism -> attribute;
    8.85 -
    8.86 -datatype slot =
    8.87 -  Slot |
    8.88 -  Value of value option |
    8.89 -  Assignable of value option Unsynchronized.ref;
    8.90 -
    8.91 -
    8.92 -(* datatype token *)
    8.93 -
    8.94 -datatype token_kind =
    8.95 -  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    8.96 -  Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
    8.97 -  Malformed | Error of string | Sync | EOF;
    8.98 -
    8.99 -datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
   8.100 -
   8.101 -val str_of_kind =
   8.102 - fn Command => "command"
   8.103 -  | Keyword => "keyword"
   8.104 -  | Ident => "identifier"
   8.105 -  | LongIdent => "long identifier"
   8.106 -  | SymIdent => "symbolic identifier"
   8.107 -  | Var => "schematic variable"
   8.108 -  | TypeIdent => "type variable"
   8.109 -  | TypeVar => "schematic type variable"
   8.110 -  | Nat => "number"
   8.111 -  | String => "string"
   8.112 -  | AltString => "back-quoted string"
   8.113 -  | Verbatim => "verbatim text"
   8.114 -  | Space => "white space"
   8.115 -  | Comment => "comment text"
   8.116 -  | InternalValue => "internal value"
   8.117 -  | Malformed => "malformed symbolic character"
   8.118 -  | Error _ => "bad input"
   8.119 -  | Sync => "sync marker"
   8.120 -  | EOF => "end-of-file";
   8.121 -
   8.122 -
   8.123 -(* position *)
   8.124 -
   8.125 -fun position_of (Token ((_, (pos, _)), _, _)) = pos;
   8.126 -fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
   8.127 -
   8.128 -val pos_of = Position.str_of o position_of;
   8.129 -
   8.130 -
   8.131 -(* control tokens *)
   8.132 -
   8.133 -fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
   8.134 -val eof = mk_eof Position.none;
   8.135 -
   8.136 -fun is_eof (Token (_, (EOF, _), _)) = true
   8.137 -  | is_eof _ = false;
   8.138 -
   8.139 -val not_eof = not o is_eof;
   8.140 -
   8.141 -fun not_sync (Token (_, (Sync, _), _)) = false
   8.142 -  | not_sync _ = true;
   8.143 -
   8.144 -val stopper =
   8.145 -  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
   8.146 -
   8.147 -
   8.148 -(* kind of token *)
   8.149 -
   8.150 -fun kind_of (Token (_, (k, _), _)) = k;
   8.151 -fun is_kind k (Token (_, (k', _), _)) = k = k';
   8.152 -
   8.153 -fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   8.154 -  | keyword_with _ _ = false;
   8.155 -
   8.156 -fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   8.157 -  | ident_with _ _ = false;
   8.158 -
   8.159 -fun is_proper (Token (_, (Space, _), _)) = false
   8.160 -  | is_proper (Token (_, (Comment, _), _)) = false
   8.161 -  | is_proper _ = true;
   8.162 -
   8.163 -fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
   8.164 -  | is_semicolon _ = false;
   8.165 -
   8.166 -fun is_comment (Token (_, (Comment, _), _)) = true
   8.167 -  | is_comment _ = false;
   8.168 -
   8.169 -fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
   8.170 -  | is_begin_ignore _ = false;
   8.171 -
   8.172 -fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
   8.173 -  | is_end_ignore _ = false;
   8.174 -
   8.175 -
   8.176 -(* blanks and newlines -- space tokens obey lines *)
   8.177 -
   8.178 -fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
   8.179 -  | is_blank _ = false;
   8.180 -
   8.181 -fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
   8.182 -  | is_newline _ = false;
   8.183 -
   8.184 -
   8.185 -(* token content *)
   8.186 -
   8.187 -fun source_of (Token ((source, (pos, _)), _, _)) =
   8.188 -  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
   8.189 -
   8.190 -fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
   8.191 -
   8.192 -fun content_of (Token (_, (_, x), _)) = x;
   8.193 -
   8.194 -
   8.195 -(* unparse *)
   8.196 -
   8.197 -fun escape q =
   8.198 -  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
   8.199 -
   8.200 -fun unparse (Token (_, (kind, x), _)) =
   8.201 -  (case kind of
   8.202 -    String => x |> quote o escape "\""
   8.203 -  | AltString => x |> enclose "`" "`" o escape "`"
   8.204 -  | Verbatim => x |> enclose "{*" "*}"
   8.205 -  | Comment => x |> enclose "(*" "*)"
   8.206 -  | Malformed => space_implode " " (explode x)
   8.207 -  | Sync => ""
   8.208 -  | EOF => ""
   8.209 -  | _ => x);
   8.210 -
   8.211 -fun text_of tok =
   8.212 -  if is_semicolon tok then ("terminator", "")
   8.213 -  else
   8.214 -    let
   8.215 -      val k = str_of_kind (kind_of tok);
   8.216 -      val s = unparse tok
   8.217 -        handle ERROR _ => Symbol.separate_chars (content_of tok);
   8.218 -    in
   8.219 -      if s = "" then (k, "")
   8.220 -      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
   8.221 -      else (k, s)
   8.222 -    end;
   8.223 -
   8.224 -
   8.225 -
   8.226 -(** associated values **)
   8.227 -
   8.228 -(* access values *)
   8.229 -
   8.230 -fun get_value (Token (_, _, Value v)) = v
   8.231 -  | get_value _ = NONE;
   8.232 -
   8.233 -fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
   8.234 -  | map_value _ tok = tok;
   8.235 -
   8.236 -
   8.237 -(* make values *)
   8.238 -
   8.239 -fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
   8.240 -
   8.241 -val mk_text = mk_value "<text>" o Text;
   8.242 -val mk_typ = mk_value "<typ>" o Typ;
   8.243 -val mk_term = mk_value "<term>" o Term;
   8.244 -val mk_fact = mk_value "<fact>" o Fact;
   8.245 -val mk_attribute = mk_value "<attribute>" o Attribute;
   8.246 -
   8.247 -
   8.248 -(* static binding *)
   8.249 -
   8.250 -(*1st stage: make empty slots assignable*)
   8.251 -fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
   8.252 -  | assignable tok = tok;
   8.253 -
   8.254 -(*2nd stage: assign values as side-effect of scanning*)
   8.255 -fun assign v (Token (_, _, Assignable r)) = r := v
   8.256 -  | assign _ _ = ();
   8.257 -
   8.258 -(*3rd stage: static closure of final values*)
   8.259 -fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
   8.260 -  | closure tok = tok;
   8.261 -
   8.262 -
   8.263 -
   8.264 -(** scanners **)
   8.265 -
   8.266 -open Basic_Symbol_Pos;
   8.267 -
   8.268 -fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
   8.269 -
   8.270 -
   8.271 -(* scan symbolic idents *)
   8.272 -
   8.273 -val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
   8.274 -
   8.275 -val scan_symid =
   8.276 -  Scan.many1 (is_sym_char o symbol) ||
   8.277 -  Scan.one (Symbol.is_symbolic o symbol) >> single;
   8.278 -
   8.279 -fun is_symid str =
   8.280 -  (case try Symbol.explode str of
   8.281 -    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
   8.282 -  | SOME ss => forall is_sym_char ss
   8.283 -  | _ => false);
   8.284 -
   8.285 -fun ident_or_symbolic "begin" = false
   8.286 -  | ident_or_symbolic ":" = true
   8.287 -  | ident_or_symbolic "::" = true
   8.288 -  | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
   8.289 -
   8.290 -
   8.291 -(* scan verbatim text *)
   8.292 -
   8.293 -val scan_verb =
   8.294 -  $$$ "*" --| Scan.ahead (~$$$ "}") ||
   8.295 -  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
   8.296 -
   8.297 -val scan_verbatim =
   8.298 -  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
   8.299 -    (Symbol_Pos.change_prompt
   8.300 -      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
   8.301 -
   8.302 -
   8.303 -(* scan space *)
   8.304 -
   8.305 -fun is_space s = Symbol.is_blank s andalso s <> "\n";
   8.306 -
   8.307 -val scan_space =
   8.308 -  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
   8.309 -  Scan.many (is_space o symbol) @@@ $$$ "\n";
   8.310 -
   8.311 -
   8.312 -(* scan comment *)
   8.313 -
   8.314 -val scan_comment =
   8.315 -  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
   8.316 -
   8.317 -
   8.318 -(* scan malformed symbols *)
   8.319 -
   8.320 -val scan_malformed =
   8.321 -  $$$ Symbol.malformed |--
   8.322 -    Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
   8.323 -  --| Scan.option ($$$ Symbol.end_malformed);
   8.324 -
   8.325 -
   8.326 -
   8.327 -(** token sources **)
   8.328 -
   8.329 -fun source_proper src = src |> Source.filter is_proper;
   8.330 -
   8.331 -local
   8.332 -
   8.333 -fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
   8.334 -
   8.335 -fun token k ss =
   8.336 -  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
   8.337 -
   8.338 -fun token_range k (pos1, (ss, pos2)) =
   8.339 -  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
   8.340 -
   8.341 -fun scan (lex1, lex2) = !!! "bad input"
   8.342 -  (Symbol_Pos.scan_string >> token_range String ||
   8.343 -    Symbol_Pos.scan_alt_string >> token_range AltString ||
   8.344 -    scan_verbatim >> token_range Verbatim ||
   8.345 -    scan_comment >> token_range Comment ||
   8.346 -    scan_space >> token Space ||
   8.347 -    scan_malformed >> token Malformed ||
   8.348 -    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
   8.349 -    (Scan.max token_leq
   8.350 -      (Scan.max token_leq
   8.351 -        (Scan.literal lex2 >> pair Command)
   8.352 -        (Scan.literal lex1 >> pair Keyword))
   8.353 -      (Syntax.scan_longid >> pair LongIdent ||
   8.354 -        Syntax.scan_id >> pair Ident ||
   8.355 -        Syntax.scan_var >> pair Var ||
   8.356 -        Syntax.scan_tid >> pair TypeIdent ||
   8.357 -        Syntax.scan_tvar >> pair TypeVar ||
   8.358 -        Syntax.scan_nat >> pair Nat ||
   8.359 -        scan_symid >> pair SymIdent) >> uncurry token));
   8.360 -
   8.361 -fun recover msg =
   8.362 -  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
   8.363 -  >> (single o token (Error msg));
   8.364 -
   8.365 -in
   8.366 -
   8.367 -fun source' {do_recover} get_lex =
   8.368 -  Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
   8.369 -    (Option.map (rpair recover) do_recover);
   8.370 -
   8.371 -fun source do_recover get_lex pos src =
   8.372 -  Symbol_Pos.source pos src
   8.373 -  |> source' do_recover get_lex;
   8.374 -
   8.375 -end;
   8.376 -
   8.377 -
   8.378 -(* read_antiq *)
   8.379 -
   8.380 -fun read_antiq lex scan (syms, pos) =
   8.381 -  let
   8.382 -    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
   8.383 -      "@{" ^ Symbol_Pos.content syms ^ "}");
   8.384 -
   8.385 -    val res =
   8.386 -      Source.of_list syms
   8.387 -      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
   8.388 -      |> source_proper
   8.389 -      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
   8.390 -      |> Source.exhaust;
   8.391 -  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
   8.392 -
   8.393 -end;
     9.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon May 17 15:05:32 2010 +0200
     9.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 17 15:11:25 2010 +0200
     9.3 @@ -25,7 +25,7 @@
     9.4    val local_theory_to_proof: string -> string -> Keyword.T ->
     9.5      (local_theory -> Proof.state) parser -> unit
     9.6    val print_outer_syntax: unit -> unit
     9.7 -  val scan: Position.T -> string -> OuterLex.token list
     9.8 +  val scan: Position.T -> string -> Token.T list
     9.9    val parse: Position.T -> string -> Toplevel.transition list
    9.10    val process_file: Path.T -> theory -> theory
    9.11    type isar
    9.12 @@ -37,11 +37,6 @@
    9.13  structure Outer_Syntax: OUTER_SYNTAX =
    9.14  struct
    9.15  
    9.16 -structure T = OuterLex;
    9.17 -type 'a parser = 'a Parse.parser;
    9.18 -
    9.19 -
    9.20 -
    9.21  (** outer syntax **)
    9.22  
    9.23  (* command parsers *)
    9.24 @@ -171,17 +166,17 @@
    9.25  fun toplevel_source term do_recover cmd src =
    9.26    let
    9.27      val no_terminator =
    9.28 -      Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.not_eof));
    9.29 +      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
    9.30      fun recover int =
    9.31        (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
    9.32    in
    9.33      src
    9.34 -    |> T.source_proper
    9.35 -    |> Source.source T.stopper
    9.36 +    |> Token.source_proper
    9.37 +    |> Source.source Token.stopper
    9.38        (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
    9.39          (Option.map recover do_recover)
    9.40      |> Source.map_filter I
    9.41 -    |> Source.source T.stopper
    9.42 +    |> Source.source Token.stopper
    9.43          (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
    9.44          (Option.map recover do_recover)
    9.45      |> Source.map_filter I
    9.46 @@ -193,13 +188,13 @@
    9.47  fun scan pos str =
    9.48    Source.of_string str
    9.49    |> Symbol.source {do_recover = false}
    9.50 -  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
    9.51 +  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
    9.52    |> Source.exhaust;
    9.53  
    9.54  fun parse pos str =
    9.55    Source.of_string str
    9.56    |> Symbol.source {do_recover = false}
    9.57 -  |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
    9.58 +  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
    9.59    |> toplevel_source false NONE get_command
    9.60    |> Source.exhaust;
    9.61  
    9.62 @@ -222,7 +217,7 @@
    9.63  
    9.64  type isar =
    9.65    (Toplevel.transition, (Toplevel.transition option,
    9.66 -    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
    9.67 +    (Token.T, (Token.T option, (Token.T, (Token.T,
    9.68        (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
    9.69    Source.source) Source.source) Source.source) Source.source)
    9.70    Source.source) Source.source) Source.source) Source.source;
    9.71 @@ -230,7 +225,7 @@
    9.72  fun isar term : isar =
    9.73    Source.tty
    9.74    |> Symbol.source {do_recover = true}
    9.75 -  |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
    9.76 +  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
    9.77    |> toplevel_source term (SOME true) get_command;
    9.78  
    9.79  
    10.1 --- a/src/Pure/Isar/parse.ML	Mon May 17 15:05:32 2010 +0200
    10.2 +++ b/src/Pure/Isar/parse.ML	Mon May 17 15:11:25 2010 +0200
    10.3 @@ -6,17 +6,16 @@
    10.4  
    10.5  signature PARSE =
    10.6  sig
    10.7 -  type token = OuterLex.token
    10.8 -  type 'a parser = token list -> 'a * token list
    10.9 -  type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
   10.10 -  val group: string -> (token list -> 'a) -> token list -> 'a
   10.11 -  val !!! : (token list -> 'a) -> token list -> 'a
   10.12 -  val !!!! : (token list -> 'a) -> token list -> 'a
   10.13 +  type 'a parser = Token.T list -> 'a * Token.T list
   10.14 +  type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
   10.15 +  val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
   10.16 +  val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
   10.17 +  val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
   10.18    val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
   10.19    val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
   10.20    val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
   10.21 -  val not_eof: token parser
   10.22 -  val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
   10.23 +  val not_eof: Token.T parser
   10.24 +  val position: (Token.T list -> 'a * 'b) -> Token.T list -> ('a * Position.T) * 'b
   10.25    val command: string parser
   10.26    val keyword: string parser
   10.27    val short_ident: string parser
   10.28 @@ -98,11 +97,8 @@
   10.29  structure Parse: PARSE =
   10.30  struct
   10.31  
   10.32 -structure T = OuterLex;
   10.33 -type token = T.token;
   10.34 -
   10.35 -type 'a parser = token list -> 'a * token list;
   10.36 -type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
   10.37 +type 'a parser = Token.T list -> 'a * Token.T list;
   10.38 +type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
   10.39  
   10.40  
   10.41  (** error handling **)
   10.42 @@ -112,9 +108,11 @@
   10.43  fun fail_with s = Scan.fail_with
   10.44    (fn [] => s ^ " expected (past end-of-file!)"
   10.45      | (tok :: _) =>
   10.46 -        (case T.text_of tok of
   10.47 -          (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
   10.48 -        | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
   10.49 +        (case Token.text_of tok of
   10.50 +          (txt, "") =>
   10.51 +            s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
   10.52 +        | (txt1, txt2) =>
   10.53 +            s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
   10.54  
   10.55  fun group s scan = scan || fail_with s;
   10.56  
   10.57 @@ -124,7 +122,7 @@
   10.58  fun cut kind scan =
   10.59    let
   10.60      fun get_pos [] = " (past end-of-file!)"
   10.61 -      | get_pos (tok :: _) = T.pos_of tok;
   10.62 +      | get_pos (tok :: _) = Token.pos_of tok;
   10.63  
   10.64      fun err (toks, NONE) = kind ^ get_pos toks
   10.65        | err (toks, SOME msg) =
   10.66 @@ -149,42 +147,42 @@
   10.67  (* tokens *)
   10.68  
   10.69  fun RESET_VALUE atom = (*required for all primitive parsers*)
   10.70 -  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
   10.71 +  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x));
   10.72  
   10.73  
   10.74 -val not_eof = RESET_VALUE (Scan.one T.not_eof);
   10.75 +val not_eof = RESET_VALUE (Scan.one Token.not_eof);
   10.76  
   10.77 -fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
   10.78 -fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
   10.79 -fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
   10.80 +fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
   10.81 +fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
   10.82 +fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
   10.83  
   10.84  fun kind k =
   10.85 -  group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
   10.86 +  group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
   10.87  
   10.88 -val command = kind T.Command;
   10.89 -val keyword = kind T.Keyword;
   10.90 -val short_ident = kind T.Ident;
   10.91 -val long_ident = kind T.LongIdent;
   10.92 -val sym_ident = kind T.SymIdent;
   10.93 -val term_var = kind T.Var;
   10.94 -val type_ident = kind T.TypeIdent;
   10.95 -val type_var = kind T.TypeVar;
   10.96 -val number = kind T.Nat;
   10.97 -val string = kind T.String;
   10.98 -val alt_string = kind T.AltString;
   10.99 -val verbatim = kind T.Verbatim;
  10.100 -val sync = kind T.Sync;
  10.101 -val eof = kind T.EOF;
  10.102 +val command = kind Token.Command;
  10.103 +val keyword = kind Token.Keyword;
  10.104 +val short_ident = kind Token.Ident;
  10.105 +val long_ident = kind Token.LongIdent;
  10.106 +val sym_ident = kind Token.SymIdent;
  10.107 +val term_var = kind Token.Var;
  10.108 +val type_ident = kind Token.TypeIdent;
  10.109 +val type_var = kind Token.TypeVar;
  10.110 +val number = kind Token.Nat;
  10.111 +val string = kind Token.String;
  10.112 +val alt_string = kind Token.AltString;
  10.113 +val verbatim = kind Token.Verbatim;
  10.114 +val sync = kind Token.Sync;
  10.115 +val eof = kind Token.EOF;
  10.116  
  10.117 -fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
  10.118 -val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
  10.119 +fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
  10.120 +val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
  10.121  
  10.122  fun $$$ x =
  10.123 -  group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
  10.124 +  group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
  10.125  
  10.126  fun reserved x =
  10.127    group ("reserved identifier " ^ quote x)
  10.128 -    (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
  10.129 +    (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
  10.130  
  10.131  val semicolon = $$$ ";";
  10.132  
    11.1 --- a/src/Pure/Isar/rule_insts.ML	Mon May 17 15:05:32 2010 +0200
    11.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon May 17 15:11:25 2010 +0200
    11.3 @@ -29,9 +29,6 @@
    11.4  structure RuleInsts: RULE_INSTS =
    11.5  struct
    11.6  
    11.7 -structure T = OuterLex;
    11.8 -
    11.9 -
   11.10  (** reading instantiations **)
   11.11  
   11.12  local
   11.13 @@ -100,11 +97,11 @@
   11.14  
   11.15      val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
   11.16      val internal_insts = term_insts |> map_filter
   11.17 -      (fn (xi, T.Term t) => SOME (xi, t)
   11.18 -        | (_, T.Text _) => NONE
   11.19 +      (fn (xi, Token.Term t) => SOME (xi, t)
   11.20 +        | (_, Token.Text _) => NONE
   11.21          | (xi, _) => error_var "Term argument expected for " xi);
   11.22      val external_insts = term_insts |> map_filter
   11.23 -      (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
   11.24 +      (fn (xi, Token.Text s) => SOME (xi, s) | _ => NONE);
   11.25  
   11.26  
   11.27      (* mixed type instantiations *)
   11.28 @@ -114,8 +111,8 @@
   11.29          val S = the_sort tvars xi;
   11.30          val T =
   11.31            (case arg of
   11.32 -            T.Text s => Syntax.read_typ ctxt s
   11.33 -          | T.Typ T => T
   11.34 +            Token.Text s => Syntax.read_typ ctxt s
   11.35 +          | Token.Typ T => T
   11.36            | _ => error_var "Type argument expected for " xi);
   11.37        in
   11.38          if Sign.of_sort thy (T, S) then ((xi, S), T)
   11.39 @@ -172,9 +169,9 @@
   11.40      val _ = (*assign internalized values*)
   11.41        mixed_insts |> List.app (fn (arg, (xi, _)) =>
   11.42          if is_tvar xi then
   11.43 -          T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
   11.44 +          Token.assign (SOME (Token.Typ (the (AList.lookup (op =) type_insts xi)))) arg
   11.45          else
   11.46 -          T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   11.47 +          Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   11.48    in
   11.49      Drule.instantiate insts thm |> Rule_Cases.save thm
   11.50    end;
   11.51 @@ -197,7 +194,7 @@
   11.52  
   11.53  fun read_instantiate ctxt args thm =
   11.54    read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
   11.55 -    (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
   11.56 +    (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
   11.57  
   11.58  fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
   11.59  
   11.60 @@ -210,9 +207,9 @@
   11.61  local
   11.62  
   11.63  val value =
   11.64 -  Args.internal_typ >> T.Typ ||
   11.65 -  Args.internal_term >> T.Term ||
   11.66 -  Args.name_source >> T.Text;
   11.67 +  Args.internal_typ >> Token.Typ ||
   11.68 +  Args.internal_term >> Token.Term ||
   11.69 +  Args.name_source >> Token.Text;
   11.70  
   11.71  val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
   11.72    >> (fn (xi, (a, v)) => (a, (xi, v)));
   11.73 @@ -233,8 +230,8 @@
   11.74  local
   11.75  
   11.76  val value =
   11.77 -  Args.internal_term >> T.Term ||
   11.78 -  Args.name_source >> T.Text;
   11.79 +  Args.internal_term >> Token.Term ||
   11.80 +  Args.name_source >> Token.Text;
   11.81  
   11.82  val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
   11.83  val concl = Args.$$$ "concl" -- Args.colon;
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/Isar/token.ML	Mon May 17 15:11:25 2010 +0200
    12.3 @@ -0,0 +1,389 @@
    12.4 +(*  Title:      Pure/Isar/token.ML
    12.5 +    Author:     Markus Wenzel, TU Muenchen
    12.6 +
    12.7 +Outer token syntax for Isabelle/Isar.
    12.8 +*)
    12.9 +
   12.10 +signature TOKEN =
   12.11 +sig
   12.12 +  datatype kind =
   12.13 +    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
   12.14 +    Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
   12.15 +    Malformed | Error of string | Sync | EOF
   12.16 +  datatype value =
   12.17 +    Text of string | Typ of typ | Term of term | Fact of thm list |
   12.18 +    Attribute of morphism -> attribute
   12.19 +  type T
   12.20 +  val str_of_kind: kind -> string
   12.21 +  val position_of: T -> Position.T
   12.22 +  val end_position_of: T -> Position.T
   12.23 +  val pos_of: T -> string
   12.24 +  val eof: T
   12.25 +  val is_eof: T -> bool
   12.26 +  val not_eof: T -> bool
   12.27 +  val not_sync: T -> bool
   12.28 +  val stopper: T Scan.stopper
   12.29 +  val kind_of: T -> kind
   12.30 +  val is_kind: kind -> T -> bool
   12.31 +  val keyword_with: (string -> bool) -> T -> bool
   12.32 +  val ident_with: (string -> bool) -> T -> bool
   12.33 +  val is_proper: T -> bool
   12.34 +  val is_semicolon: T -> bool
   12.35 +  val is_comment: T -> bool
   12.36 +  val is_begin_ignore: T -> bool
   12.37 +  val is_end_ignore: T -> bool
   12.38 +  val is_blank: T -> bool
   12.39 +  val is_newline: T -> bool
   12.40 +  val source_of: T -> string
   12.41 +  val source_position_of: T -> Symbol_Pos.text * Position.T
   12.42 +  val content_of: T -> string
   12.43 +  val unparse: T -> string
   12.44 +  val text_of: T -> string * string
   12.45 +  val get_value: T -> value option
   12.46 +  val map_value: (value -> value) -> T -> T
   12.47 +  val mk_text: string -> T
   12.48 +  val mk_typ: typ -> T
   12.49 +  val mk_term: term -> T
   12.50 +  val mk_fact: thm list -> T
   12.51 +  val mk_attribute: (morphism -> attribute) -> T
   12.52 +  val assignable: T -> T
   12.53 +  val assign: value option -> T -> unit
   12.54 +  val closure: T -> T
   12.55 +  val ident_or_symbolic: string -> bool
   12.56 +  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
   12.57 +  val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
   12.58 +  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
   12.59 +    (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
   12.60 +  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
   12.61 +    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
   12.62 +      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   12.63 +  val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
   12.64 +end;
   12.65 +
   12.66 +structure Token: TOKEN =
   12.67 +struct
   12.68 +
   12.69 +(** tokens **)
   12.70 +
   12.71 +(* token values *)
   12.72 +
   12.73 +(*The value slot assigns an (optional) internal value to a token,
   12.74 +  usually as a side-effect of special scanner setup (see also
   12.75 +  args.ML).  Note that an assignable ref designates an intermediate
   12.76 +  state of internalization -- it is NOT meant to persist.*)
   12.77 +
   12.78 +datatype value =
   12.79 +  Text of string |
   12.80 +  Typ of typ |
   12.81 +  Term of term |
   12.82 +  Fact of thm list |
   12.83 +  Attribute of morphism -> attribute;
   12.84 +
   12.85 +datatype slot =
   12.86 +  Slot |
   12.87 +  Value of value option |
   12.88 +  Assignable of value option Unsynchronized.ref;
   12.89 +
   12.90 +
   12.91 +(* datatype token *)
   12.92 +
   12.93 +datatype kind =
   12.94 +  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
   12.95 +  Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
   12.96 +  Malformed | Error of string | Sync | EOF;
   12.97 +
   12.98 +datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
   12.99 +
  12.100 +val str_of_kind =
  12.101 + fn Command => "command"
  12.102 +  | Keyword => "keyword"
  12.103 +  | Ident => "identifier"
  12.104 +  | LongIdent => "long identifier"
  12.105 +  | SymIdent => "symbolic identifier"
  12.106 +  | Var => "schematic variable"
  12.107 +  | TypeIdent => "type variable"
  12.108 +  | TypeVar => "schematic type variable"
  12.109 +  | Nat => "number"
  12.110 +  | String => "string"
  12.111 +  | AltString => "back-quoted string"
  12.112 +  | Verbatim => "verbatim text"
  12.113 +  | Space => "white space"
  12.114 +  | Comment => "comment text"
  12.115 +  | InternalValue => "internal value"
  12.116 +  | Malformed => "malformed symbolic character"
  12.117 +  | Error _ => "bad input"
  12.118 +  | Sync => "sync marker"
  12.119 +  | EOF => "end-of-file";
  12.120 +
  12.121 +
  12.122 +(* position *)
  12.123 +
  12.124 +fun position_of (Token ((_, (pos, _)), _, _)) = pos;
  12.125 +fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
  12.126 +
  12.127 +val pos_of = Position.str_of o position_of;
  12.128 +
  12.129 +
  12.130 +(* control tokens *)
  12.131 +
  12.132 +fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
  12.133 +val eof = mk_eof Position.none;
  12.134 +
  12.135 +fun is_eof (Token (_, (EOF, _), _)) = true
  12.136 +  | is_eof _ = false;
  12.137 +
  12.138 +val not_eof = not o is_eof;
  12.139 +
  12.140 +fun not_sync (Token (_, (Sync, _), _)) = false
  12.141 +  | not_sync _ = true;
  12.142 +
  12.143 +val stopper =
  12.144 +  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
  12.145 +
  12.146 +
  12.147 +(* kind of token *)
  12.148 +
  12.149 +fun kind_of (Token (_, (k, _), _)) = k;
  12.150 +fun is_kind k (Token (_, (k', _), _)) = k = k';
  12.151 +
  12.152 +fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
  12.153 +  | keyword_with _ _ = false;
  12.154 +
  12.155 +fun ident_with pred (Token (_, (Ident, x), _)) = pred x
  12.156 +  | ident_with _ _ = false;
  12.157 +
  12.158 +fun is_proper (Token (_, (Space, _), _)) = false
  12.159 +  | is_proper (Token (_, (Comment, _), _)) = false
  12.160 +  | is_proper _ = true;
  12.161 +
  12.162 +fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
  12.163 +  | is_semicolon _ = false;
  12.164 +
  12.165 +fun is_comment (Token (_, (Comment, _), _)) = true
  12.166 +  | is_comment _ = false;
  12.167 +
  12.168 +fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
  12.169 +  | is_begin_ignore _ = false;
  12.170 +
  12.171 +fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
  12.172 +  | is_end_ignore _ = false;
  12.173 +
  12.174 +
  12.175 +(* blanks and newlines -- space tokens obey lines *)
  12.176 +
  12.177 +fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
  12.178 +  | is_blank _ = false;
  12.179 +
  12.180 +fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
  12.181 +  | is_newline _ = false;
  12.182 +
  12.183 +
  12.184 +(* token content *)
  12.185 +
  12.186 +fun source_of (Token ((source, (pos, _)), _, _)) =
  12.187 +  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
  12.188 +
  12.189 +fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
  12.190 +
  12.191 +fun content_of (Token (_, (_, x), _)) = x;
  12.192 +
  12.193 +
  12.194 +(* unparse *)
  12.195 +
  12.196 +fun escape q =
  12.197 +  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
  12.198 +
  12.199 +fun unparse (Token (_, (kind, x), _)) =
  12.200 +  (case kind of
  12.201 +    String => x |> quote o escape "\""
  12.202 +  | AltString => x |> enclose "`" "`" o escape "`"
  12.203 +  | Verbatim => x |> enclose "{*" "*}"
  12.204 +  | Comment => x |> enclose "(*" "*)"
  12.205 +  | Malformed => space_implode " " (explode x)
  12.206 +  | Sync => ""
  12.207 +  | EOF => ""
  12.208 +  | _ => x);
  12.209 +
  12.210 +fun text_of tok =
  12.211 +  if is_semicolon tok then ("terminator", "")
  12.212 +  else
  12.213 +    let
  12.214 +      val k = str_of_kind (kind_of tok);
  12.215 +      val s = unparse tok
  12.216 +        handle ERROR _ => Symbol.separate_chars (content_of tok);
  12.217 +    in
  12.218 +      if s = "" then (k, "")
  12.219 +      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
  12.220 +      else (k, s)
  12.221 +    end;
  12.222 +
  12.223 +
  12.224 +
  12.225 +(** associated values **)
  12.226 +
  12.227 +(* access values *)
  12.228 +
  12.229 +fun get_value (Token (_, _, Value v)) = v
  12.230 +  | get_value _ = NONE;
  12.231 +
  12.232 +fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
  12.233 +  | map_value _ tok = tok;
  12.234 +
  12.235 +
  12.236 +(* make values *)
  12.237 +
  12.238 +fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
  12.239 +
  12.240 +val mk_text = mk_value "<text>" o Text;
  12.241 +val mk_typ = mk_value "<typ>" o Typ;
  12.242 +val mk_term = mk_value "<term>" o Term;
  12.243 +val mk_fact = mk_value "<fact>" o Fact;
  12.244 +val mk_attribute = mk_value "<attribute>" o Attribute;
  12.245 +
  12.246 +
  12.247 +(* static binding *)
  12.248 +
  12.249 +(*1st stage: make empty slots assignable*)
  12.250 +fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
  12.251 +  | assignable tok = tok;
  12.252 +
  12.253 +(*2nd stage: assign values as side-effect of scanning*)
  12.254 +fun assign v (Token (_, _, Assignable r)) = r := v
  12.255 +  | assign _ _ = ();
  12.256 +
  12.257 +(*3rd stage: static closure of final values*)
  12.258 +fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
  12.259 +  | closure tok = tok;
  12.260 +
  12.261 +
  12.262 +
  12.263 +(** scanners **)
  12.264 +
  12.265 +open Basic_Symbol_Pos;
  12.266 +
  12.267 +fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
  12.268 +
  12.269 +
  12.270 +(* scan symbolic idents *)
  12.271 +
  12.272 +val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
  12.273 +
  12.274 +val scan_symid =
  12.275 +  Scan.many1 (is_sym_char o symbol) ||
  12.276 +  Scan.one (Symbol.is_symbolic o symbol) >> single;
  12.277 +
  12.278 +fun is_symid str =
  12.279 +  (case try Symbol.explode str of
  12.280 +    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
  12.281 +  | SOME ss => forall is_sym_char ss
  12.282 +  | _ => false);
  12.283 +
  12.284 +fun ident_or_symbolic "begin" = false
  12.285 +  | ident_or_symbolic ":" = true
  12.286 +  | ident_or_symbolic "::" = true
  12.287 +  | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
  12.288 +
  12.289 +
  12.290 +(* scan verbatim text *)
  12.291 +
  12.292 +val scan_verb =
  12.293 +  $$$ "*" --| Scan.ahead (~$$$ "}") ||
  12.294 +  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
  12.295 +
  12.296 +val scan_verbatim =
  12.297 +  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
  12.298 +    (Symbol_Pos.change_prompt
  12.299 +      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
  12.300 +
  12.301 +
  12.302 +(* scan space *)
  12.303 +
  12.304 +fun is_space s = Symbol.is_blank s andalso s <> "\n";
  12.305 +
  12.306 +val scan_space =
  12.307 +  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
  12.308 +  Scan.many (is_space o symbol) @@@ $$$ "\n";
  12.309 +
  12.310 +
  12.311 +(* scan comment *)
  12.312 +
  12.313 +val scan_comment =
  12.314 +  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
  12.315 +
  12.316 +
  12.317 +(* scan malformed symbols *)
  12.318 +
  12.319 +val scan_malformed =
  12.320 +  $$$ Symbol.malformed |--
  12.321 +    Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
  12.322 +  --| Scan.option ($$$ Symbol.end_malformed);
  12.323 +
  12.324 +
  12.325 +
  12.326 +(** token sources **)
  12.327 +
  12.328 +fun source_proper src = src |> Source.filter is_proper;
  12.329 +
  12.330 +local
  12.331 +
  12.332 +fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
  12.333 +
  12.334 +fun token k ss =
  12.335 +  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
  12.336 +
  12.337 +fun token_range k (pos1, (ss, pos2)) =
  12.338 +  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
  12.339 +
  12.340 +fun scan (lex1, lex2) = !!! "bad input"
  12.341 +  (Symbol_Pos.scan_string >> token_range String ||
  12.342 +    Symbol_Pos.scan_alt_string >> token_range AltString ||
  12.343 +    scan_verbatim >> token_range Verbatim ||
  12.344 +    scan_comment >> token_range Comment ||
  12.345 +    scan_space >> token Space ||
  12.346 +    scan_malformed >> token Malformed ||
  12.347 +    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
  12.348 +    (Scan.max token_leq
  12.349 +      (Scan.max token_leq
  12.350 +        (Scan.literal lex2 >> pair Command)
  12.351 +        (Scan.literal lex1 >> pair Keyword))
  12.352 +      (Syntax.scan_longid >> pair LongIdent ||
  12.353 +        Syntax.scan_id >> pair Ident ||
  12.354 +        Syntax.scan_var >> pair Var ||
  12.355 +        Syntax.scan_tid >> pair TypeIdent ||
  12.356 +        Syntax.scan_tvar >> pair TypeVar ||
  12.357 +        Syntax.scan_nat >> pair Nat ||
  12.358 +        scan_symid >> pair SymIdent) >> uncurry token));
  12.359 +
  12.360 +fun recover msg =
  12.361 +  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
  12.362 +  >> (single o token (Error msg));
  12.363 +
  12.364 +in
  12.365 +
  12.366 +fun source' {do_recover} get_lex =
  12.367 +  Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
  12.368 +    (Option.map (rpair recover) do_recover);
  12.369 +
  12.370 +fun source do_recover get_lex pos src =
  12.371 +  Symbol_Pos.source pos src
  12.372 +  |> source' do_recover get_lex;
  12.373 +
  12.374 +end;
  12.375 +
  12.376 +
  12.377 +(* read_antiq *)
  12.378 +
  12.379 +fun read_antiq lex scan (syms, pos) =
  12.380 +  let
  12.381 +    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
  12.382 +      "@{" ^ Symbol_Pos.content syms ^ "}");
  12.383 +
  12.384 +    val res =
  12.385 +      Source.of_list syms
  12.386 +      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
  12.387 +      |> source_proper
  12.388 +      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
  12.389 +      |> Source.exhaust;
  12.390 +  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
  12.391 +
  12.392 +end;
    13.1 --- a/src/Pure/ML/ml_context.ML	Mon May 17 15:05:32 2010 +0200
    13.2 +++ b/src/Pure/ML/ml_context.ML	Mon May 17 15:11:25 2010 +0200
    13.3 @@ -112,8 +112,6 @@
    13.4  
    13.5  local
    13.6  
    13.7 -structure T = OuterLex;
    13.8 -
    13.9  val antiq =
   13.10    Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
   13.11    >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   13.12 @@ -144,7 +142,8 @@
   13.13              | expand (Antiquote.Antiq (ss, range)) (scope, background) =
   13.14                  let
   13.15                    val context = Stack.top scope;
   13.16 -                  val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
   13.17 +                  val (f, context') =
   13.18 +                    antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
   13.19                    val (decl, background') = f background;
   13.20                    val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
   13.21                  in (decl', (Stack.map_top (K context') scope, background')) end
    14.1 --- a/src/Pure/ROOT.ML	Mon May 17 15:05:32 2010 +0200
    14.2 +++ b/src/Pure/ROOT.ML	Mon May 17 15:11:25 2010 +0200
    14.3 @@ -167,7 +167,7 @@
    14.4  use "Proof/proofchecker.ML";
    14.5  
    14.6  (*outer syntax*)
    14.7 -use "Isar/outer_lex.ML";
    14.8 +use "Isar/token.ML";
    14.9  use "Isar/keyword.ML";
   14.10  use "Isar/parse.ML";
   14.11  use "Isar/parse_value.ML";
   14.12 @@ -299,6 +299,13 @@
   14.13  struct
   14.14  
   14.15  structure OuterKeyword = Keyword;
   14.16 +
   14.17 +structure OuterLex =
   14.18 +struct
   14.19 +  open Token;
   14.20 +  type token = T;
   14.21 +end;
   14.22 +
   14.23  structure OuterParse = Parse;
   14.24  structure OuterSyntax = Outer_Syntax;
   14.25  structure SpecParse = Parse_Spec;
    15.1 --- a/src/Pure/Thy/latex.ML	Mon May 17 15:05:32 2010 +0200
    15.2 +++ b/src/Pure/Thy/latex.ML	Mon May 17 15:11:25 2010 +0200
    15.3 @@ -9,7 +9,7 @@
    15.4    val output_known_symbols: (string -> bool) * (string -> bool) ->
    15.5      Symbol.symbol list -> string
    15.6    val output_symbols: Symbol.symbol list -> string
    15.7 -  val output_basic: OuterLex.token -> string
    15.8 +  val output_basic: Token.T -> string
    15.9    val output_markup: string -> string -> string
   15.10    val output_markup_env: string -> string -> string
   15.11    val output_verbatim: string -> string
   15.12 @@ -99,24 +99,22 @@
   15.13  
   15.14  (* token output *)
   15.15  
   15.16 -structure T = OuterLex;
   15.17 -
   15.18 -val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
   15.19 +val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
   15.20  
   15.21  fun output_basic tok =
   15.22 -  let val s = T.content_of tok in
   15.23 +  let val s = Token.content_of tok in
   15.24      if invisible_token tok then ""
   15.25 -    else if T.is_kind T.Command tok then
   15.26 +    else if Token.is_kind Token.Command tok then
   15.27        "\\isacommand{" ^ output_syms s ^ "}"
   15.28 -    else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
   15.29 +    else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
   15.30        "\\isakeyword{" ^ output_syms s ^ "}"
   15.31 -    else if T.is_kind T.String tok then
   15.32 +    else if Token.is_kind Token.String tok then
   15.33        enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   15.34 -    else if T.is_kind T.AltString tok then
   15.35 +    else if Token.is_kind Token.AltString tok then
   15.36        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   15.37 -    else if T.is_kind T.Verbatim tok then
   15.38 +    else if Token.is_kind Token.Verbatim tok then
   15.39        let
   15.40 -        val (txt, pos) = T.source_position_of tok;
   15.41 +        val (txt, pos) = Token.source_position_of tok;
   15.42          val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   15.43          val out = implode (map output_syms_antiq ants);
   15.44        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    16.1 --- a/src/Pure/Thy/thy_header.ML	Mon May 17 15:05:32 2010 +0200
    16.2 +++ b/src/Pure/Thy/thy_header.ML	Mon May 17 15:11:25 2010 +0200
    16.3 @@ -6,17 +6,13 @@
    16.4  
    16.5  signature THY_HEADER =
    16.6  sig
    16.7 -  val args: OuterLex.token list ->
    16.8 -    (string * string list * (string * bool) list) * OuterLex.token list
    16.9 +  val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   16.10    val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
   16.11  end;
   16.12  
   16.13  structure Thy_Header: THY_HEADER =
   16.14  struct
   16.15  
   16.16 -structure T = OuterLex;
   16.17 -
   16.18 -
   16.19  (* keywords *)
   16.20  
   16.21  val headerN = "header";
   16.22 @@ -58,9 +54,9 @@
   16.23    let val res =
   16.24      src
   16.25      |> Symbol.source {do_recover = false}
   16.26 -    |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
   16.27 -    |> T.source_proper
   16.28 -    |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
   16.29 +    |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
   16.30 +    |> Token.source_proper
   16.31 +    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
   16.32      |> Source.get_single;
   16.33    in
   16.34      (case res of SOME (x, _) => x
    17.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 17 15:05:32 2010 +0200
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 17 15:11:25 2010 +0200
    17.3 @@ -24,7 +24,7 @@
    17.4    val modes: string list Unsynchronized.ref
    17.5    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    17.6    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    17.7 -    (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    17.8 +    (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
    17.9    val pretty_text: string -> Pretty.T
   17.10    val pretty_term: Proof.context -> term -> Pretty.T
   17.11    val pretty_thm: Proof.context -> thm -> Pretty.T
   17.12 @@ -36,9 +36,6 @@
   17.13  structure ThyOutput: THY_OUTPUT =
   17.14  struct
   17.15  
   17.16 -structure T = OuterLex;
   17.17 -
   17.18 -
   17.19  (** global options **)
   17.20  
   17.21  val display = Unsynchronized.ref false;
   17.22 @@ -154,7 +151,7 @@
   17.23    let
   17.24      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
   17.25        | expand (Antiquote.Antiq (ss, (pos, _))) =
   17.26 -          let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
   17.27 +          let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
   17.28              options opts (fn () => command src state) ();  (*preview errors!*)
   17.29              PrintMode.with_modes (! modes @ Latex.modes)
   17.30                (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
   17.31 @@ -178,7 +175,7 @@
   17.32  
   17.33  datatype token =
   17.34      NoToken
   17.35 -  | BasicToken of T.token
   17.36 +  | BasicToken of Token.T
   17.37    | MarkupToken of string * (string * Position.T)
   17.38    | MarkupEnvToken of string * (string * Position.T)
   17.39    | VerbatimToken of string * Position.T;
   17.40 @@ -195,10 +192,10 @@
   17.41  fun basic_token pred (BasicToken tok) = pred tok
   17.42    | basic_token _ _ = false;
   17.43  
   17.44 -val improper_token = basic_token (not o T.is_proper);
   17.45 -val comment_token = basic_token T.is_comment;
   17.46 -val blank_token = basic_token T.is_blank;
   17.47 -val newline_token = basic_token T.is_newline;
   17.48 +val improper_token = basic_token (not o Token.is_proper);
   17.49 +val comment_token = basic_token Token.is_comment;
   17.50 +val blank_token = basic_token Token.is_blank;
   17.51 +val newline_token = basic_token Token.is_newline;
   17.52  
   17.53  
   17.54  (* command spans *)
   17.55 @@ -303,19 +300,19 @@
   17.56  local
   17.57  
   17.58  val space_proper =
   17.59 -  Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
   17.60 +  Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
   17.61  
   17.62 -val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
   17.63 +val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
   17.64  val improper = Scan.many is_improper;
   17.65  val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
   17.66 -val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
   17.67 +val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
   17.68  
   17.69 -val opt_newline = Scan.option (Scan.one T.is_newline);
   17.70 +val opt_newline = Scan.option (Scan.one Token.is_newline);
   17.71  
   17.72  val ignore =
   17.73 -  Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
   17.74 +  Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
   17.75      >> pair (d + 1)) ||
   17.76 -  Scan.depend (fn d => Scan.one T.is_end_ignore --|
   17.77 +  Scan.depend (fn d => Scan.one Token.is_end_ignore --|
   17.78      (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
   17.79      >> pair (d - 1));
   17.80  
   17.81 @@ -336,18 +333,19 @@
   17.82  
   17.83      fun markup mark mk flag = Scan.peek (fn d =>
   17.84        improper |--
   17.85 -        Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
   17.86 +        Parse.position
   17.87 +          (Scan.one (Token.is_kind Token.Command andf is_markup mark o Token.content_of)) --
   17.88        Scan.repeat tag --
   17.89        Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
   17.90        >> (fn (((tok, pos), tags), txt) =>
   17.91 -        let val name = T.content_of tok
   17.92 +        let val name = Token.content_of tok
   17.93          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
   17.94  
   17.95      val command = Scan.peek (fn d =>
   17.96 -      Parse.position (Scan.one (T.is_kind T.Command)) --
   17.97 +      Parse.position (Scan.one (Token.is_kind Token.Command)) --
   17.98        Scan.repeat tag
   17.99        >> (fn ((tok, pos), tags) =>
  17.100 -        let val name = T.content_of tok
  17.101 +        let val name = Token.content_of tok
  17.102          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
  17.103  
  17.104      val cmt = Scan.peek (fn d =>
  17.105 @@ -367,8 +365,8 @@
  17.106  
  17.107      (* spans *)
  17.108  
  17.109 -    val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
  17.110 -    val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
  17.111 +    val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
  17.112 +    val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
  17.113  
  17.114      val cmd = Scan.one (is_some o fst);
  17.115      val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
  17.116 @@ -390,8 +388,8 @@
  17.117  
  17.118      val spans =
  17.119        src
  17.120 -      |> Source.filter (not o T.is_semicolon)
  17.121 -      |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
  17.122 +      |> Source.filter (not o Token.is_semicolon)
  17.123 +      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
  17.124        |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
  17.125        |> Source.exhaust;
  17.126  
  17.127 @@ -490,7 +488,7 @@
  17.128  
  17.129  (* default output *)
  17.130  
  17.131 -val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
  17.132 +val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
  17.133  
  17.134  fun maybe_pretty_source pretty src xs =
  17.135    map pretty xs  (*always pretty in order to exhibit errors!*)
    18.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon May 17 15:05:32 2010 +0200
    18.2 +++ b/src/Pure/Thy/thy_syntax.ML	Mon May 17 15:11:25 2010 +0200
    18.3 @@ -7,18 +7,17 @@
    18.4  signature THY_SYNTAX =
    18.5  sig
    18.6    val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
    18.7 -    (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
    18.8 +    (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
    18.9        Source.source) Source.source) Source.source) Source.source
   18.10 -  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
   18.11 -  val present_token: OuterLex.token -> output
   18.12 -  val report_token: OuterLex.token -> unit
   18.13 +  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
   18.14 +  val present_token: Token.T -> output
   18.15 +  val report_token: Token.T -> unit
   18.16    datatype span_kind = Command of string | Ignored | Malformed
   18.17    type span
   18.18    val span_kind: span -> span_kind
   18.19 -  val span_content: span -> OuterLex.token list
   18.20 +  val span_content: span -> Token.T list
   18.21    val span_range: span -> Position.range
   18.22 -  val span_source: (OuterLex.token, 'a) Source.source ->
   18.23 -    (span, (OuterLex.token, 'a) Source.source) Source.source
   18.24 +  val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
   18.25    val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   18.26    val present_span: span -> output
   18.27    val report_span: span -> unit
   18.28 @@ -29,16 +28,13 @@
   18.29  structure ThySyntax: THY_SYNTAX =
   18.30  struct
   18.31  
   18.32 -structure T = OuterLex;
   18.33 -
   18.34 -
   18.35  (** tokens **)
   18.36  
   18.37  (* parse *)
   18.38  
   18.39  fun token_source lexs pos src =
   18.40    Symbol.source {do_recover = true} src
   18.41 -  |> T.source {do_recover = SOME false} (K lexs) pos;
   18.42 +  |> Token.source {do_recover = SOME false} (K lexs) pos;
   18.43  
   18.44  fun parse_tokens lexs pos str =
   18.45    Source.of_string str
   18.46 @@ -51,33 +47,33 @@
   18.47  local
   18.48  
   18.49  val token_kind_markup =
   18.50 - fn T.Command       => (Markup.commandN, [])
   18.51 -  | T.Keyword       => (Markup.keywordN, [])
   18.52 -  | T.Ident         => Markup.ident
   18.53 -  | T.LongIdent     => Markup.ident
   18.54 -  | T.SymIdent      => Markup.ident
   18.55 -  | T.Var           => Markup.var
   18.56 -  | T.TypeIdent     => Markup.tfree
   18.57 -  | T.TypeVar       => Markup.tvar
   18.58 -  | T.Nat           => Markup.ident
   18.59 -  | T.String        => Markup.string
   18.60 -  | T.AltString     => Markup.altstring
   18.61 -  | T.Verbatim      => Markup.verbatim
   18.62 -  | T.Space         => Markup.none
   18.63 -  | T.Comment       => Markup.comment
   18.64 -  | T.InternalValue => Markup.none
   18.65 -  | T.Malformed     => Markup.malformed
   18.66 -  | T.Error _       => Markup.malformed
   18.67 -  | T.Sync          => Markup.control
   18.68 -  | T.EOF           => Markup.control;
   18.69 + fn Token.Command       => (Markup.commandN, [])
   18.70 +  | Token.Keyword       => (Markup.keywordN, [])
   18.71 +  | Token.Ident         => Markup.ident
   18.72 +  | Token.LongIdent     => Markup.ident
   18.73 +  | Token.SymIdent      => Markup.ident
   18.74 +  | Token.Var           => Markup.var
   18.75 +  | Token.TypeIdent     => Markup.tfree
   18.76 +  | Token.TypeVar       => Markup.tvar
   18.77 +  | Token.Nat           => Markup.ident
   18.78 +  | Token.String        => Markup.string
   18.79 +  | Token.AltString     => Markup.altstring
   18.80 +  | Token.Verbatim      => Markup.verbatim
   18.81 +  | Token.Space         => Markup.none
   18.82 +  | Token.Comment       => Markup.comment
   18.83 +  | Token.InternalValue => Markup.none
   18.84 +  | Token.Malformed     => Markup.malformed
   18.85 +  | Token.Error _       => Markup.malformed
   18.86 +  | Token.Sync          => Markup.control
   18.87 +  | Token.EOF           => Markup.control;
   18.88  
   18.89  in
   18.90  
   18.91  fun present_token tok =
   18.92 -  Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
   18.93 +  Markup.enclose (token_kind_markup (Token.kind_of tok)) (Output.output (Token.unparse tok));
   18.94  
   18.95  fun report_token tok =
   18.96 -  Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
   18.97 +  Position.report (token_kind_markup (Token.kind_of tok)) (Token.position_of tok);
   18.98  
   18.99  end;
  18.100  
  18.101 @@ -88,7 +84,7 @@
  18.102  (* type span *)
  18.103  
  18.104  datatype span_kind = Command of string | Ignored | Malformed;
  18.105 -datatype span = Span of span_kind * OuterLex.token list;
  18.106 +datatype span = Span of span_kind * Token.T list;
  18.107  
  18.108  fun span_kind (Span (k, _)) = k;
  18.109  fun span_content (Span (_, toks)) = toks;
  18.110 @@ -98,8 +94,8 @@
  18.111      [] => (Position.none, Position.none)
  18.112    | toks =>
  18.113        let
  18.114 -        val start_pos = T.position_of (hd toks);
  18.115 -        val end_pos = T.end_position_of (List.last toks);
  18.116 +        val start_pos = Token.position_of (hd toks);
  18.117 +        val end_pos = Token.end_position_of (List.last toks);
  18.118        in (start_pos, end_pos) end);
  18.119  
  18.120  
  18.121 @@ -107,7 +103,7 @@
  18.122  
  18.123  local
  18.124  
  18.125 -val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
  18.126 +val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
  18.127  
  18.128  val body =
  18.129    Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
  18.130 @@ -120,7 +116,7 @@
  18.131  
  18.132  in
  18.133  
  18.134 -fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
  18.135 +fun span_source src = Source.source Token.stopper (Scan.bulk span) NONE src;
  18.136  
  18.137  end;
  18.138  
    19.1 --- a/src/Tools/Code/code_printer.ML	Mon May 17 15:05:32 2010 +0200
    19.2 +++ b/src/Tools/Code/code_printer.ML	Mon May 17 15:11:25 2010 +0200
    19.3 @@ -72,9 +72,9 @@
    19.4    val parse_infix: ('a -> 'b) -> lrx * int -> string
    19.5      -> int * ((fixity -> 'b -> Pretty.T)
    19.6      -> fixity -> 'a list -> Pretty.T)
    19.7 -  val parse_syntax: ('a -> 'b) -> OuterParse.token list
    19.8 +  val parse_syntax: ('a -> 'b) -> Token.T list
    19.9      -> (int * ((fixity -> 'b -> Pretty.T)
   19.10 -    -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
   19.11 +    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
   19.12    val simple_const_syntax: simple_const_syntax -> proto_const_syntax
   19.13    val activate_const_syntax: theory -> literals
   19.14      -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    20.1 --- a/src/Tools/Code/code_target.ML	Mon May 17 15:05:32 2010 +0200
    20.2 +++ b/src/Tools/Code/code_target.ML	Mon May 17 15:11:25 2010 +0200
    20.3 @@ -19,14 +19,13 @@
    20.4  
    20.5    type destination
    20.6    type serialization
    20.7 -  val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
    20.8 -    -> OuterLex.token list -> 'a
    20.9 +  val parse_args: 'a parser -> Token.T list -> 'a
   20.10    val stmt_names_of_destination: destination -> string list
   20.11    val mk_serialization: string -> ('a -> unit) option
   20.12      -> (Path.T option -> 'a -> unit)
   20.13      -> ('a -> string * string option list)
   20.14      -> 'a -> serialization
   20.15 -  val serialize: theory -> string -> int option -> string option -> OuterLex.token list
   20.16 +  val serialize: theory -> string -> int option -> string option -> Token.T list
   20.17      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   20.18    val serialize_custom: theory -> string * (serializer * literals)
   20.19      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   20.20 @@ -105,7 +104,7 @@
   20.21  
   20.22  type serializer =
   20.23    string option                         (*module name*)
   20.24 -  -> OuterLex.token list                (*arguments*)
   20.25 +  -> Token.T list                       (*arguments*)
   20.26    -> (string -> string)                 (*labelled_name*)
   20.27    -> string list                        (*reserved symbols*)
   20.28    -> (string * Pretty.T) list           (*includes*)
   20.29 @@ -498,7 +497,7 @@
   20.30  val allow_abort_cmd = gen_allow_abort Code.read_const;
   20.31  
   20.32  fun parse_args f args =
   20.33 -  case Scan.read OuterLex.stopper f args
   20.34 +  case Scan.read Token.stopper f args
   20.35     of SOME x => x
   20.36      | NONE => error "Bad serializer arguments";
   20.37  
   20.38 @@ -575,8 +574,8 @@
   20.39      K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   20.40  
   20.41  fun shell_command thyname cmd = Toplevel.program (fn _ =>
   20.42 -  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
   20.43 -    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
   20.44 +  (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
   20.45 +    ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
   20.46     of SOME f => (writeln "Now generating code..."; f (theory thyname))
   20.47      | NONE => error ("Bad directive " ^ quote cmd)))
   20.48    handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    21.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 15:05:32 2010 +0200
    21.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 17 15:11:25 2010 +0200
    21.3 @@ -195,7 +195,7 @@
    21.4        query
    21.5        |> (fn s => s ^ ";")
    21.6        |> OuterSyntax.scan Position.start
    21.7 -      |> filter OuterLex.is_proper
    21.8 +      |> filter Token.is_proper
    21.9        |> Scan.error parse_query
   21.10        |> fst;
   21.11