renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;
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 + val import_segment: (theory -> theory) parser
2.10 + val import_theory : (theory -> theory) parser
2.11 + val end_import : (theory -> theory) parser
2.12 +
2.13 + val setup_theory : (theory -> theory) parser
2.14 + val end_setup : (theory -> theory) parser
2.15 +
2.16 + val thm_maps : (theory -> theory) parser
2.17 + val ignore_thms : (theory -> theory) parser
2.18 + val type_maps : (theory -> theory) parser
2.19 + val def_maps : (theory -> theory) parser
2.20 + val const_maps : (theory -> theory) parser
2.21 + val const_moves : (theory -> theory) parser
2.22 + val const_renames : (theory -> theory) parser
2.23
2.24 - val import_segment: token list -> (theory -> theory) * token list
2.25 - val import_theory : token list -> (theory -> theory) * token list
2.26 - val end_import : token list -> (theory -> theory) * token list
2.27 -
2.28 - val setup_theory : token list -> (theory -> theory) * token list
2.29 - val end_setup : token list -> (theory -> theory) * token list
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 T.Text s => s);
5.130 -val internal_typ = value (fn T.Typ T => T);
5.131 -val internal_term = value (fn T.Term t => t);
5.132 -val internal_fact = value (fn T.Fact ths => ths);
5.133 -val internal_attribute = value (fn T.Attribute att => att);
5.134 +val internal_text = value (fn Token.Text s => s);
5.135 +val internal_typ = value (fn Token.Typ T => T);
5.136 +val internal_term = value (fn Token.Term t => t);
5.137 +val internal_fact = value (fn Token.Fact ths => ths);
5.138 +val internal_attribute = value (fn Token.Attribute att => att);
5.139
5.140 -fun named_text intern = internal_text || named >> evaluate T.Text (intern o T.content_of);
5.141 -fun named_typ readT = internal_typ || named >> evaluate T.Typ (readT o T.source_of);
5.142 -fun named_term read = internal_term || named >> evaluate T.Term (read o T.source_of);
5.143 -fun named_fact get = internal_fact || named >> evaluate T.Fact (get o T.content_of) ||
5.144 - alt_string >> evaluate T.Fact (get o T.source_of);
5.145 -fun named_attribute att = internal_attribute || named >> evaluate T.Attribute (att o T.content_of);
5.146 +fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
5.147 +fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
5.148 +fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
5.149 +fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
5.150 + alt_string >> evaluate Token.Fact (get o Token.source_of);
5.151 +fun named_attribute att =
5.152 + internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
5.153
5.154
5.155 (* terms and types *)
5.156 @@ -243,7 +237,7 @@
5.157 (token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
5.158 in (args, args1) end;
5.159
5.160 -val parse = #1 (parse_args T.ident_or_symbolic) false;
5.161 +val parse = #1 (parse_args Token.ident_or_symbolic) false;
5.162 fun parse1 is_symid = #2 (parse_args is_symid) false;
5.163
5.164
5.165 @@ -252,7 +246,7 @@
5.166 fun attribs intern =
5.167 let
5.168 val attrib_name = internal_text || (symbolic || named)
5.169 - >> evaluate T.Text (intern o T.content_of);
5.170 + >> evaluate Token.Text (intern o Token.content_of);
5.171 val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
5.172 in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
5.173
5.174 @@ -273,11 +267,11 @@
5.175 (** syntax wrapper **)
5.176
5.177 fun syntax kind scan (Src ((s, args), pos)) st =
5.178 - (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
5.179 + (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
5.180 (SOME x, (st', [])) => (x, st')
5.181 | (_, (_, args')) =>
5.182 error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^
5.183 - space_implode " " (map T.unparse args')));
5.184 + space_implode " " (map Token.unparse args')));
5.185
5.186 fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
5.187
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