renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;
--- a/NEWS Mon May 17 15:05:32 2010 +0200
+++ b/NEWS Mon May 17 15:11:25 2010 +0200
@@ -505,9 +505,10 @@
* Renamed some important ML structures, while keeping the old names as
legacy aliases for some time:
+ OuterKeyword ~> Keyword
+ OuterLex ~> Token
+ OuterParse ~> Parse
OuterSyntax ~> Outer_Syntax
- OuterKeyword ~> Keyword
- OuterParse ~> Parse
SpecParse ~> Parse_Spec
--- a/src/HOL/Import/import_syntax.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML Mon May 17 15:11:25 2010 +0200
@@ -4,26 +4,23 @@
signature HOL4_IMPORT_SYNTAX =
sig
- type token = OuterLex.token
- type command = token list -> (theory -> theory) * token list
-
- val import_segment: token list -> (theory -> theory) * token list
- val import_theory : token list -> (theory -> theory) * token list
- val end_import : token list -> (theory -> theory) * token list
-
- val setup_theory : token list -> (theory -> theory) * token list
- val end_setup : token list -> (theory -> theory) * token list
+ val import_segment: (theory -> theory) parser
+ val import_theory : (theory -> theory) parser
+ val end_import : (theory -> theory) parser
+
+ val setup_theory : (theory -> theory) parser
+ val end_setup : (theory -> theory) parser
+
+ val thm_maps : (theory -> theory) parser
+ val ignore_thms : (theory -> theory) parser
+ val type_maps : (theory -> theory) parser
+ val def_maps : (theory -> theory) parser
+ val const_maps : (theory -> theory) parser
+ val const_moves : (theory -> theory) parser
+ val const_renames : (theory -> theory) parser
- val thm_maps : token list -> (theory -> theory) * token list
- val ignore_thms : token list -> (theory -> theory) * token list
- val type_maps : token list -> (theory -> theory) * token list
- val def_maps : token list -> (theory -> theory) * token list
- val const_maps : token list -> (theory -> theory) * token list
- val const_moves : token list -> (theory -> theory) * token list
- val const_renames : token list -> (theory -> theory) * token list
-
- val skip_import_dir : token list -> (theory -> theory) * token list
- val skip_import : token list -> (theory -> theory) * token list
+ val skip_import_dir : (theory -> theory) parser
+ val skip_import : (theory -> theory) parser
val setup : unit -> unit
end
@@ -31,9 +28,6 @@
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
struct
-type token = OuterLex.token
-type command = token list -> (theory -> theory) * token list
-
local structure P = OuterParse and K = OuterKeyword in
(* Parsers *)
@@ -48,11 +42,11 @@
|> add_dump (";setup_theory " ^ thyname))
fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
-val skip_import_dir : command = P.string >> do_skip_import_dir
+val skip_import_dir = P.string >> do_skip_import_dir
val lower = String.map Char.toLower
fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
-val skip_import : command = P.short_ident >> do_skip_import
+val skip_import = P.short_ident >> do_skip_import
fun end_import toks =
Scan.succeed
@@ -160,8 +154,8 @@
(Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
Scan.empty_lexicon)
val get_lexes = fn () => !lexes
- val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
- val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
+ val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
+ val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 15:11:25 2010 +0200
@@ -335,9 +335,9 @@
in
Source.of_string name
|> Symbol.source {do_recover=false}
- |> OuterLex.source {do_recover=SOME false} lex Position.start
- |> OuterLex.source_proper
- |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
|> Source.exhaust
end
--- a/src/Pure/IsaMakefile Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/IsaMakefile Mon May 17 15:11:25 2010 +0200
@@ -67,24 +67,25 @@
Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \
Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML \
+ Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML \
Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML \
Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML \
- ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
- ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
- ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
- ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
- Proof/extraction.ML Proof/proof_rewrite_rules.ML \
- Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
- ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
- ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
- ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
- ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
- ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
+ Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML \
+ Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
+ ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
+ ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
+ ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
+ ML-Systems/use_context.ML Proof/extraction.ML \
+ Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
+ Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
+ ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
+ ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
+ ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
+ ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
+ ProofGeneral/proof_general_emacs.ML \
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
--- a/src/Pure/Isar/args.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Isar/args.ML Mon May 17 15:11:25 2010 +0200
@@ -7,10 +7,9 @@
signature ARGS =
sig
- type token = OuterLex.token
type src
- val src: (string * token list) * Position.T -> src
- val dest_src: src -> (string * token list) * Position.T
+ val src: (string * Token.T list) * Position.T -> src
+ val dest_src: src -> (string * Token.T list) * Position.T
val pretty_src: Proof.context -> src -> Pretty.T
val map_name: (string -> string) -> src -> src
val morph_values: morphism -> src -> src
@@ -57,8 +56,8 @@
val const: bool -> string context_parser
val const_proper: bool -> string context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
- val parse: token list parser
- val parse1: (string -> bool) -> token list parser
+ val parse: Token.T list parser
+ val parse1: (string -> bool) -> Token.T list parser
val attribs: (string -> string) -> src list parser
val opt_attribs: (string -> string) -> src list parser
val thm_name: (string -> string) -> string -> (binding * src list) parser
@@ -70,15 +69,9 @@
structure Args: ARGS =
struct
-structure T = OuterLex;
-
-type token = T.token;
-
-
-
(** datatype src **)
-datatype src = Src of (string * token list) * Position.T;
+datatype src = Src of (string * Token.T list) * Position.T;
val src = Src;
fun dest_src (Src src) = src;
@@ -87,12 +80,12 @@
let
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
fun prt arg =
- (case T.get_value arg of
- SOME (T.Text s) => Pretty.str (quote s)
- | SOME (T.Typ T) => Syntax.pretty_typ ctxt T
- | SOME (T.Term t) => Syntax.pretty_term ctxt t
- | SOME (T.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
- | _ => Pretty.str (T.unparse arg));
+ (case Token.get_value arg of
+ SOME (Token.Text s) => Pretty.str (quote s)
+ | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
+ | SOME (Token.Term t) => Syntax.pretty_term ctxt t
+ | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
+ | _ => Pretty.str (Token.unparse arg));
val (s, args) = #1 (dest_src src);
in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
@@ -102,15 +95,15 @@
(* values *)
-fun morph_values phi = map_args (T.map_value
- (fn T.Text s => T.Text s
- | T.Typ T => T.Typ (Morphism.typ phi T)
- | T.Term t => T.Term (Morphism.term phi t)
- | T.Fact ths => T.Fact (Morphism.fact phi ths)
- | T.Attribute att => T.Attribute (Morphism.transform phi att)));
+fun morph_values phi = map_args (Token.map_value
+ (fn Token.Text s => Token.Text s
+ | Token.Typ T => Token.Typ (Morphism.typ phi T)
+ | Token.Term t => Token.Term (Morphism.term phi t)
+ | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
+ | Token.Attribute att => Token.Attribute (Morphism.transform phi att)));
-val assignable = map_args T.assignable;
-val closure = map_args T.closure;
+val assignable = map_args Token.assignable;
+val closure = map_args Token.closure;
@@ -134,7 +127,7 @@
val alt_string = token Parse.alt_string;
val symbolic = token Parse.keyword_ident_or_symbolic;
-fun $$$ x = (ident >> T.content_of || Parse.keyword)
+fun $$$ x = (ident >> Token.content_of || Parse.keyword)
:|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
@@ -153,39 +146,40 @@
fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
-val name_source = named >> T.source_of;
-val name_source_position = named >> T.source_position_of;
+val name_source = named >> Token.source_of;
+val name_source_position = named >> Token.source_position_of;
-val name = named >> T.content_of;
+val name = named >> Token.content_of;
val binding = Parse.position name >> Binding.make;
-val alt_name = alt_string >> T.content_of;
-val symbol = symbolic >> T.content_of;
+val alt_name = alt_string >> Token.content_of;
+val symbol = symbolic >> Token.content_of;
val liberal_name = symbol || name;
-val var = (ident >> T.content_of) :|-- (fn x =>
+val var = (ident >> Token.content_of) :|-- (fn x =>
(case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
(* values *)
fun value dest = Scan.some (fn arg =>
- (case T.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
+ (case Token.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
fun evaluate mk eval arg =
- let val x = eval arg in (T.assign (SOME (mk x)) arg; x) end;
+ let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
+
+val internal_text = value (fn Token.Text s => s);
+val internal_typ = value (fn Token.Typ T => T);
+val internal_term = value (fn Token.Term t => t);
+val internal_fact = value (fn Token.Fact ths => ths);
+val internal_attribute = value (fn Token.Attribute att => att);
-val internal_text = value (fn T.Text s => s);
-val internal_typ = value (fn T.Typ T => T);
-val internal_term = value (fn T.Term t => t);
-val internal_fact = value (fn T.Fact ths => ths);
-val internal_attribute = value (fn T.Attribute att => att);
-
-fun named_text intern = internal_text || named >> evaluate T.Text (intern o T.content_of);
-fun named_typ readT = internal_typ || named >> evaluate T.Typ (readT o T.source_of);
-fun named_term read = internal_term || named >> evaluate T.Term (read o T.source_of);
-fun named_fact get = internal_fact || named >> evaluate T.Fact (get o T.content_of) ||
- alt_string >> evaluate T.Fact (get o T.source_of);
-fun named_attribute att = internal_attribute || named >> evaluate T.Attribute (att o T.content_of);
+fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
+fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
+fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
+fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
+ alt_string >> evaluate Token.Fact (get o Token.source_of);
+fun named_attribute att =
+ internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
(* terms and types *)
@@ -243,7 +237,7 @@
(token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
in (args, args1) end;
-val parse = #1 (parse_args T.ident_or_symbolic) false;
+val parse = #1 (parse_args Token.ident_or_symbolic) false;
fun parse1 is_symid = #2 (parse_args is_symid) false;
@@ -252,7 +246,7 @@
fun attribs intern =
let
val attrib_name = internal_text || (symbolic || named)
- >> evaluate T.Text (intern o T.content_of);
+ >> evaluate Token.Text (intern o Token.content_of);
val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
@@ -273,11 +267,11 @@
(** syntax wrapper **)
fun syntax kind scan (Src ((s, args), pos)) st =
- (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
+ (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
(SOME x, (st', [])) => (x, st')
| (_, (_, args')) =>
error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^
- space_implode " " (map T.unparse args')));
+ space_implode " " (map Token.unparse args')));
fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
--- a/src/Pure/Isar/attrib.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Mon May 17 15:11:25 2010 +0200
@@ -47,9 +47,6 @@
structure Attrib: ATTRIB =
struct
-structure T = OuterLex;
-
-
(* source and bindings *)
type src = Args.src;
@@ -216,7 +213,7 @@
(* internal *)
-fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
+fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
(* rule composition *)
--- a/src/Pure/Isar/method.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Isar/method.ML Mon May 17 15:11:25 2010 +0200
@@ -411,7 +411,7 @@
(* outer parser *)
fun is_symid_meth s =
- s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s;
+ s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
local
--- a/src/Pure/Isar/outer_lex.ML Mon May 17 15:05:32 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-(* Title: Pure/Isar/outer_lex.ML
- Author: Markus Wenzel, TU Muenchen
-
-Outer lexical syntax for Isabelle/Isar.
-*)
-
-signature OUTER_LEX =
-sig
- datatype token_kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
- Malformed | Error of string | Sync | EOF
- datatype value =
- Text of string | Typ of typ | Term of term | Fact of thm list |
- Attribute of morphism -> attribute
- type token
- val str_of_kind: token_kind -> string
- val position_of: token -> Position.T
- val end_position_of: token -> Position.T
- val pos_of: token -> string
- val eof: token
- val is_eof: token -> bool
- val not_eof: token -> bool
- val not_sync: token -> bool
- val stopper: token Scan.stopper
- val kind_of: token -> token_kind
- val is_kind: token_kind -> token -> bool
- val keyword_with: (string -> bool) -> token -> bool
- val ident_with: (string -> bool) -> token -> bool
- val is_proper: token -> bool
- val is_semicolon: token -> bool
- val is_comment: token -> bool
- val is_begin_ignore: token -> bool
- val is_end_ignore: token -> bool
- val is_blank: token -> bool
- val is_newline: token -> bool
- val source_of: token -> string
- val source_position_of: token -> Symbol_Pos.text * Position.T
- val content_of: token -> string
- val unparse: token -> string
- val text_of: token -> string * string
- val get_value: token -> value option
- val map_value: (value -> value) -> token -> token
- val mk_text: string -> token
- val mk_typ: typ -> token
- val mk_term: term -> token
- val mk_fact: thm list -> token
- val mk_attribute: (morphism -> attribute) -> token
- val assignable: token -> token
- val assign: value option -> token -> unit
- val closure: token -> token
- val ident_or_symbolic: string -> bool
- val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
- val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
- val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
- (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
- val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
- Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
- (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
- val read_antiq: Scan.lexicon -> (token list -> 'a * token list) ->
- Symbol_Pos.T list * Position.T -> 'a
-end;
-
-structure OuterLex: OUTER_LEX =
-struct
-
-(** tokens **)
-
-(* token values *)
-
-(*The value slot assigns an (optional) internal value to a token,
- usually as a side-effect of special scanner setup (see also
- args.ML). Note that an assignable ref designates an intermediate
- state of internalization -- it is NOT meant to persist.*)
-
-datatype value =
- Text of string |
- Typ of typ |
- Term of term |
- Fact of thm list |
- Attribute of morphism -> attribute;
-
-datatype slot =
- Slot |
- Value of value option |
- Assignable of value option Unsynchronized.ref;
-
-
-(* datatype token *)
-
-datatype token_kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
- Malformed | Error of string | Sync | EOF;
-
-datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
-
-val str_of_kind =
- fn Command => "command"
- | Keyword => "keyword"
- | Ident => "identifier"
- | LongIdent => "long identifier"
- | SymIdent => "symbolic identifier"
- | Var => "schematic variable"
- | TypeIdent => "type variable"
- | TypeVar => "schematic type variable"
- | Nat => "number"
- | String => "string"
- | AltString => "back-quoted string"
- | Verbatim => "verbatim text"
- | Space => "white space"
- | Comment => "comment text"
- | InternalValue => "internal value"
- | Malformed => "malformed symbolic character"
- | Error _ => "bad input"
- | Sync => "sync marker"
- | EOF => "end-of-file";
-
-
-(* position *)
-
-fun position_of (Token ((_, (pos, _)), _, _)) = pos;
-fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
-
-val pos_of = Position.str_of o position_of;
-
-
-(* control tokens *)
-
-fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
-val eof = mk_eof Position.none;
-
-fun is_eof (Token (_, (EOF, _), _)) = true
- | is_eof _ = false;
-
-val not_eof = not o is_eof;
-
-fun not_sync (Token (_, (Sync, _), _)) = false
- | not_sync _ = true;
-
-val stopper =
- Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
-
-
-(* kind of token *)
-
-fun kind_of (Token (_, (k, _), _)) = k;
-fun is_kind k (Token (_, (k', _), _)) = k = k';
-
-fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
- | keyword_with _ _ = false;
-
-fun ident_with pred (Token (_, (Ident, x), _)) = pred x
- | ident_with _ _ = false;
-
-fun is_proper (Token (_, (Space, _), _)) = false
- | is_proper (Token (_, (Comment, _), _)) = false
- | is_proper _ = true;
-
-fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
- | is_semicolon _ = false;
-
-fun is_comment (Token (_, (Comment, _), _)) = true
- | is_comment _ = false;
-
-fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
- | is_begin_ignore _ = false;
-
-fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
- | is_end_ignore _ = false;
-
-
-(* blanks and newlines -- space tokens obey lines *)
-
-fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
- | is_blank _ = false;
-
-fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
- | is_newline _ = false;
-
-
-(* token content *)
-
-fun source_of (Token ((source, (pos, _)), _, _)) =
- YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
-
-fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
-
-fun content_of (Token (_, (_, x), _)) = x;
-
-
-(* unparse *)
-
-fun escape q =
- implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
-
-fun unparse (Token (_, (kind, x), _)) =
- (case kind of
- String => x |> quote o escape "\""
- | AltString => x |> enclose "`" "`" o escape "`"
- | Verbatim => x |> enclose "{*" "*}"
- | Comment => x |> enclose "(*" "*)"
- | Malformed => space_implode " " (explode x)
- | Sync => ""
- | EOF => ""
- | _ => x);
-
-fun text_of tok =
- if is_semicolon tok then ("terminator", "")
- else
- let
- val k = str_of_kind (kind_of tok);
- val s = unparse tok
- handle ERROR _ => Symbol.separate_chars (content_of tok);
- in
- if s = "" then (k, "")
- else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
- else (k, s)
- end;
-
-
-
-(** associated values **)
-
-(* access values *)
-
-fun get_value (Token (_, _, Value v)) = v
- | get_value _ = NONE;
-
-fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
- | map_value _ tok = tok;
-
-
-(* make values *)
-
-fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
-
-val mk_text = mk_value "<text>" o Text;
-val mk_typ = mk_value "<typ>" o Typ;
-val mk_term = mk_value "<term>" o Term;
-val mk_fact = mk_value "<fact>" o Fact;
-val mk_attribute = mk_value "<attribute>" o Attribute;
-
-
-(* static binding *)
-
-(*1st stage: make empty slots assignable*)
-fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
- | assignable tok = tok;
-
-(*2nd stage: assign values as side-effect of scanning*)
-fun assign v (Token (_, _, Assignable r)) = r := v
- | assign _ _ = ();
-
-(*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
- | closure tok = tok;
-
-
-
-(** scanners **)
-
-open Basic_Symbol_Pos;
-
-fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
-
-
-(* scan symbolic idents *)
-
-val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
-
-val scan_symid =
- Scan.many1 (is_sym_char o symbol) ||
- Scan.one (Symbol.is_symbolic o symbol) >> single;
-
-fun is_symid str =
- (case try Symbol.explode str of
- SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
- | SOME ss => forall is_sym_char ss
- | _ => false);
-
-fun ident_or_symbolic "begin" = false
- | ident_or_symbolic ":" = true
- | ident_or_symbolic "::" = true
- | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
-
-
-(* scan verbatim text *)
-
-val scan_verb =
- $$$ "*" --| Scan.ahead (~$$$ "}") ||
- Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
-
-val scan_verbatim =
- (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
- (Symbol_Pos.change_prompt
- ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
-
-
-(* scan space *)
-
-fun is_space s = Symbol.is_blank s andalso s <> "\n";
-
-val scan_space =
- Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
- Scan.many (is_space o symbol) @@@ $$$ "\n";
-
-
-(* scan comment *)
-
-val scan_comment =
- Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
-
-
-(* scan malformed symbols *)
-
-val scan_malformed =
- $$$ Symbol.malformed |--
- Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
- --| Scan.option ($$$ Symbol.end_malformed);
-
-
-
-(** token sources **)
-
-fun source_proper src = src |> Source.filter is_proper;
-
-local
-
-fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
-
-fun token k ss =
- Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
-
-fun token_range k (pos1, (ss, pos2)) =
- Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
-
-fun scan (lex1, lex2) = !!! "bad input"
- (Symbol_Pos.scan_string >> token_range String ||
- Symbol_Pos.scan_alt_string >> token_range AltString ||
- scan_verbatim >> token_range Verbatim ||
- scan_comment >> token_range Comment ||
- scan_space >> token Space ||
- scan_malformed >> token Malformed ||
- Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
- (Scan.max token_leq
- (Scan.max token_leq
- (Scan.literal lex2 >> pair Command)
- (Scan.literal lex1 >> pair Keyword))
- (Syntax.scan_longid >> pair LongIdent ||
- Syntax.scan_id >> pair Ident ||
- Syntax.scan_var >> pair Var ||
- Syntax.scan_tid >> pair TypeIdent ||
- Syntax.scan_tvar >> pair TypeVar ||
- Syntax.scan_nat >> pair Nat ||
- scan_symid >> pair SymIdent) >> uncurry token));
-
-fun recover msg =
- Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
- >> (single o token (Error msg));
-
-in
-
-fun source' {do_recover} get_lex =
- Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
- (Option.map (rpair recover) do_recover);
-
-fun source do_recover get_lex pos src =
- Symbol_Pos.source pos src
- |> source' do_recover get_lex;
-
-end;
-
-
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
- let
- fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
- "@{" ^ Symbol_Pos.content syms ^ "}");
-
- val res =
- Source.of_list syms
- |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
- |> source_proper
- |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
- |> Source.exhaust;
- in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-end;
--- a/src/Pure/Isar/outer_syntax.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon May 17 15:11:25 2010 +0200
@@ -25,7 +25,7 @@
val local_theory_to_proof: string -> string -> Keyword.T ->
(local_theory -> Proof.state) parser -> unit
val print_outer_syntax: unit -> unit
- val scan: Position.T -> string -> OuterLex.token list
+ val scan: Position.T -> string -> Token.T list
val parse: Position.T -> string -> Toplevel.transition list
val process_file: Path.T -> theory -> theory
type isar
@@ -37,11 +37,6 @@
structure Outer_Syntax: OUTER_SYNTAX =
struct
-structure T = OuterLex;
-type 'a parser = 'a Parse.parser;
-
-
-
(** outer syntax **)
(* command parsers *)
@@ -171,17 +166,17 @@
fun toplevel_source term do_recover cmd src =
let
val no_terminator =
- Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.not_eof));
+ Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
fun recover int =
(int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
in
src
- |> T.source_proper
- |> Source.source T.stopper
+ |> Token.source_proper
+ |> Source.source Token.stopper
(Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
(Option.map recover do_recover)
|> Source.map_filter I
- |> Source.source T.stopper
+ |> Source.source Token.stopper
(Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
(Option.map recover do_recover)
|> Source.map_filter I
@@ -193,13 +188,13 @@
fun scan pos str =
Source.of_string str
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
+ |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
|> Source.exhaust;
fun parse pos str =
Source.of_string str
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
+ |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
|> toplevel_source false NONE get_command
|> Source.exhaust;
@@ -222,7 +217,7 @@
type isar =
(Toplevel.transition, (Toplevel.transition option,
- (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
+ (Token.T, (Token.T option, (Token.T, (Token.T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
Source.source) Source.source) Source.source) Source.source)
Source.source) Source.source) Source.source) Source.source;
@@ -230,7 +225,7 @@
fun isar term : isar =
Source.tty
|> Symbol.source {do_recover = true}
- |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
+ |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
|> toplevel_source term (SOME true) get_command;
--- a/src/Pure/Isar/parse.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Isar/parse.ML Mon May 17 15:11:25 2010 +0200
@@ -6,17 +6,16 @@
signature PARSE =
sig
- type token = OuterLex.token
- type 'a parser = token list -> 'a * token list
- type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
- val group: string -> (token list -> 'a) -> token list -> 'a
- val !!! : (token list -> 'a) -> token list -> 'a
- val !!!! : (token list -> 'a) -> token list -> 'a
+ type 'a parser = Token.T list -> 'a * Token.T list
+ type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
+ val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
+ val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
+ val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
- val not_eof: token parser
- val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
+ val not_eof: Token.T parser
+ val position: (Token.T list -> 'a * 'b) -> Token.T list -> ('a * Position.T) * 'b
val command: string parser
val keyword: string parser
val short_ident: string parser
@@ -98,11 +97,8 @@
structure Parse: PARSE =
struct
-structure T = OuterLex;
-type token = T.token;
-
-type 'a parser = token list -> 'a * token list;
-type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
+type 'a parser = Token.T list -> 'a * Token.T list;
+type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
(** error handling **)
@@ -112,9 +108,11 @@
fun fail_with s = Scan.fail_with
(fn [] => s ^ " expected (past end-of-file!)"
| (tok :: _) =>
- (case T.text_of tok of
- (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
- | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
+ (case Token.text_of tok of
+ (txt, "") =>
+ s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+ | (txt1, txt2) =>
+ s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
fun group s scan = scan || fail_with s;
@@ -124,7 +122,7 @@
fun cut kind scan =
let
fun get_pos [] = " (past end-of-file!)"
- | get_pos (tok :: _) = T.pos_of tok;
+ | get_pos (tok :: _) = Token.pos_of tok;
fun err (toks, NONE) = kind ^ get_pos toks
| err (toks, SOME msg) =
@@ -149,42 +147,42 @@
(* tokens *)
fun RESET_VALUE atom = (*required for all primitive parsers*)
- Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
+ Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x));
-val not_eof = RESET_VALUE (Scan.one T.not_eof);
+val not_eof = RESET_VALUE (Scan.one Token.not_eof);
-fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
-fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
-fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
+fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
+fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
+fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
fun kind k =
- group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
+ group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
-val command = kind T.Command;
-val keyword = kind T.Keyword;
-val short_ident = kind T.Ident;
-val long_ident = kind T.LongIdent;
-val sym_ident = kind T.SymIdent;
-val term_var = kind T.Var;
-val type_ident = kind T.TypeIdent;
-val type_var = kind T.TypeVar;
-val number = kind T.Nat;
-val string = kind T.String;
-val alt_string = kind T.AltString;
-val verbatim = kind T.Verbatim;
-val sync = kind T.Sync;
-val eof = kind T.EOF;
+val command = kind Token.Command;
+val keyword = kind Token.Keyword;
+val short_ident = kind Token.Ident;
+val long_ident = kind Token.LongIdent;
+val sym_ident = kind Token.SymIdent;
+val term_var = kind Token.Var;
+val type_ident = kind Token.TypeIdent;
+val type_var = kind Token.TypeVar;
+val number = kind Token.Nat;
+val string = kind Token.String;
+val alt_string = kind Token.AltString;
+val verbatim = kind Token.Verbatim;
+val sync = kind Token.Sync;
+val eof = kind Token.EOF;
-fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
-val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
+fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
+val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
fun $$$ x =
- group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
+ group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
fun reserved x =
group ("reserved identifier " ^ quote x)
- (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
+ (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
val semicolon = $$$ ";";
--- a/src/Pure/Isar/rule_insts.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML Mon May 17 15:11:25 2010 +0200
@@ -29,9 +29,6 @@
structure RuleInsts: RULE_INSTS =
struct
-structure T = OuterLex;
-
-
(** reading instantiations **)
local
@@ -100,11 +97,11 @@
val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
val internal_insts = term_insts |> map_filter
- (fn (xi, T.Term t) => SOME (xi, t)
- | (_, T.Text _) => NONE
+ (fn (xi, Token.Term t) => SOME (xi, t)
+ | (_, Token.Text _) => NONE
| (xi, _) => error_var "Term argument expected for " xi);
val external_insts = term_insts |> map_filter
- (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
+ (fn (xi, Token.Text s) => SOME (xi, s) | _ => NONE);
(* mixed type instantiations *)
@@ -114,8 +111,8 @@
val S = the_sort tvars xi;
val T =
(case arg of
- T.Text s => Syntax.read_typ ctxt s
- | T.Typ T => T
+ Token.Text s => Syntax.read_typ ctxt s
+ | Token.Typ T => T
| _ => error_var "Type argument expected for " xi);
in
if Sign.of_sort thy (T, S) then ((xi, S), T)
@@ -172,9 +169,9 @@
val _ = (*assign internalized values*)
mixed_insts |> List.app (fn (arg, (xi, _)) =>
if is_tvar xi then
- T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
+ Token.assign (SOME (Token.Typ (the (AList.lookup (op =) type_insts xi)))) arg
else
- T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
+ Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
in
Drule.instantiate insts thm |> Rule_Cases.save thm
end;
@@ -197,7 +194,7 @@
fun read_instantiate ctxt args thm =
read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *)
- (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
+ (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
@@ -210,9 +207,9 @@
local
val value =
- Args.internal_typ >> T.Typ ||
- Args.internal_term >> T.Term ||
- Args.name_source >> T.Text;
+ Args.internal_typ >> Token.Typ ||
+ Args.internal_term >> Token.Term ||
+ Args.name_source >> Token.Text;
val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
>> (fn (xi, (a, v)) => (a, (xi, v)));
@@ -233,8 +230,8 @@
local
val value =
- Args.internal_term >> T.Term ||
- Args.name_source >> T.Text;
+ Args.internal_term >> Token.Term ||
+ Args.name_source >> Token.Text;
val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
val concl = Args.$$$ "concl" -- Args.colon;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/token.ML Mon May 17 15:11:25 2010 +0200
@@ -0,0 +1,389 @@
+(* Title: Pure/Isar/token.ML
+ Author: Markus Wenzel, TU Muenchen
+
+Outer token syntax for Isabelle/Isar.
+*)
+
+signature TOKEN =
+sig
+ datatype kind =
+ Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
+ Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+ Malformed | Error of string | Sync | EOF
+ datatype value =
+ Text of string | Typ of typ | Term of term | Fact of thm list |
+ Attribute of morphism -> attribute
+ type T
+ val str_of_kind: kind -> string
+ val position_of: T -> Position.T
+ val end_position_of: T -> Position.T
+ val pos_of: T -> string
+ val eof: T
+ val is_eof: T -> bool
+ val not_eof: T -> bool
+ val not_sync: T -> bool
+ val stopper: T Scan.stopper
+ val kind_of: T -> kind
+ val is_kind: kind -> T -> bool
+ val keyword_with: (string -> bool) -> T -> bool
+ val ident_with: (string -> bool) -> T -> bool
+ val is_proper: T -> bool
+ val is_semicolon: T -> bool
+ val is_comment: T -> bool
+ val is_begin_ignore: T -> bool
+ val is_end_ignore: T -> bool
+ val is_blank: T -> bool
+ val is_newline: T -> bool
+ val source_of: T -> string
+ val source_position_of: T -> Symbol_Pos.text * Position.T
+ val content_of: T -> string
+ val unparse: T -> string
+ val text_of: T -> string * string
+ val get_value: T -> value option
+ val map_value: (value -> value) -> T -> T
+ val mk_text: string -> T
+ val mk_typ: typ -> T
+ val mk_term: term -> T
+ val mk_fact: thm list -> T
+ val mk_attribute: (morphism -> attribute) -> T
+ val assignable: T -> T
+ val assign: value option -> T -> unit
+ val closure: T -> T
+ val ident_or_symbolic: string -> bool
+ val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
+ val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
+ val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
+ val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
+ (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+ val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
+end;
+
+structure Token: TOKEN =
+struct
+
+(** tokens **)
+
+(* token values *)
+
+(*The value slot assigns an (optional) internal value to a token,
+ usually as a side-effect of special scanner setup (see also
+ args.ML). Note that an assignable ref designates an intermediate
+ state of internalization -- it is NOT meant to persist.*)
+
+datatype value =
+ Text of string |
+ Typ of typ |
+ Term of term |
+ Fact of thm list |
+ Attribute of morphism -> attribute;
+
+datatype slot =
+ Slot |
+ Value of value option |
+ Assignable of value option Unsynchronized.ref;
+
+
+(* datatype token *)
+
+datatype kind =
+ Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
+ Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+ Malformed | Error of string | Sync | EOF;
+
+datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
+
+val str_of_kind =
+ fn Command => "command"
+ | Keyword => "keyword"
+ | Ident => "identifier"
+ | LongIdent => "long identifier"
+ | SymIdent => "symbolic identifier"
+ | Var => "schematic variable"
+ | TypeIdent => "type variable"
+ | TypeVar => "schematic type variable"
+ | Nat => "number"
+ | String => "string"
+ | AltString => "back-quoted string"
+ | Verbatim => "verbatim text"
+ | Space => "white space"
+ | Comment => "comment text"
+ | InternalValue => "internal value"
+ | Malformed => "malformed symbolic character"
+ | Error _ => "bad input"
+ | Sync => "sync marker"
+ | EOF => "end-of-file";
+
+
+(* position *)
+
+fun position_of (Token ((_, (pos, _)), _, _)) = pos;
+fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
+
+val pos_of = Position.str_of o position_of;
+
+
+(* control tokens *)
+
+fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
+val eof = mk_eof Position.none;
+
+fun is_eof (Token (_, (EOF, _), _)) = true
+ | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+fun not_sync (Token (_, (Sync, _), _)) = false
+ | not_sync _ = true;
+
+val stopper =
+ Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+
+
+(* kind of token *)
+
+fun kind_of (Token (_, (k, _), _)) = k;
+fun is_kind k (Token (_, (k', _), _)) = k = k';
+
+fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
+ | keyword_with _ _ = false;
+
+fun ident_with pred (Token (_, (Ident, x), _)) = pred x
+ | ident_with _ _ = false;
+
+fun is_proper (Token (_, (Space, _), _)) = false
+ | is_proper (Token (_, (Comment, _), _)) = false
+ | is_proper _ = true;
+
+fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
+ | is_semicolon _ = false;
+
+fun is_comment (Token (_, (Comment, _), _)) = true
+ | is_comment _ = false;
+
+fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
+ | is_begin_ignore _ = false;
+
+fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
+ | is_end_ignore _ = false;
+
+
+(* blanks and newlines -- space tokens obey lines *)
+
+fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
+ | is_blank _ = false;
+
+fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
+ | is_newline _ = false;
+
+
+(* token content *)
+
+fun source_of (Token ((source, (pos, _)), _, _)) =
+ YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
+
+fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
+
+fun content_of (Token (_, (_, x), _)) = x;
+
+
+(* unparse *)
+
+fun escape q =
+ implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
+
+fun unparse (Token (_, (kind, x), _)) =
+ (case kind of
+ String => x |> quote o escape "\""
+ | AltString => x |> enclose "`" "`" o escape "`"
+ | Verbatim => x |> enclose "{*" "*}"
+ | Comment => x |> enclose "(*" "*)"
+ | Malformed => space_implode " " (explode x)
+ | Sync => ""
+ | EOF => ""
+ | _ => x);
+
+fun text_of tok =
+ if is_semicolon tok then ("terminator", "")
+ else
+ let
+ val k = str_of_kind (kind_of tok);
+ val s = unparse tok
+ handle ERROR _ => Symbol.separate_chars (content_of tok);
+ in
+ if s = "" then (k, "")
+ else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
+ else (k, s)
+ end;
+
+
+
+(** associated values **)
+
+(* access values *)
+
+fun get_value (Token (_, _, Value v)) = v
+ | get_value _ = NONE;
+
+fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
+ | map_value _ tok = tok;
+
+
+(* make values *)
+
+fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
+
+val mk_text = mk_value "<text>" o Text;
+val mk_typ = mk_value "<typ>" o Typ;
+val mk_term = mk_value "<term>" o Term;
+val mk_fact = mk_value "<fact>" o Fact;
+val mk_attribute = mk_value "<attribute>" o Attribute;
+
+
+(* static binding *)
+
+(*1st stage: make empty slots assignable*)
+fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
+ | assignable tok = tok;
+
+(*2nd stage: assign values as side-effect of scanning*)
+fun assign v (Token (_, _, Assignable r)) = r := v
+ | assign _ _ = ();
+
+(*3rd stage: static closure of final values*)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
+ | closure tok = tok;
+
+
+
+(** scanners **)
+
+open Basic_Symbol_Pos;
+
+fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
+
+
+(* scan symbolic idents *)
+
+val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
+
+val scan_symid =
+ Scan.many1 (is_sym_char o symbol) ||
+ Scan.one (Symbol.is_symbolic o symbol) >> single;
+
+fun is_symid str =
+ (case try Symbol.explode str of
+ SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
+ | SOME ss => forall is_sym_char ss
+ | _ => false);
+
+fun ident_or_symbolic "begin" = false
+ | ident_or_symbolic ":" = true
+ | ident_or_symbolic "::" = true
+ | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
+
+
+(* scan verbatim text *)
+
+val scan_verb =
+ $$$ "*" --| Scan.ahead (~$$$ "}") ||
+ Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
+
+val scan_verbatim =
+ (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
+ (Symbol_Pos.change_prompt
+ ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+
+
+(* scan space *)
+
+fun is_space s = Symbol.is_blank s andalso s <> "\n";
+
+val scan_space =
+ Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
+ Scan.many (is_space o symbol) @@@ $$$ "\n";
+
+
+(* scan comment *)
+
+val scan_comment =
+ Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
+
+
+(* scan malformed symbols *)
+
+val scan_malformed =
+ $$$ Symbol.malformed |--
+ Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
+ --| Scan.option ($$$ Symbol.end_malformed);
+
+
+
+(** token sources **)
+
+fun source_proper src = src |> Source.filter is_proper;
+
+local
+
+fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
+
+fun token k ss =
+ Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
+
+fun token_range k (pos1, (ss, pos2)) =
+ Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
+
+fun scan (lex1, lex2) = !!! "bad input"
+ (Symbol_Pos.scan_string >> token_range String ||
+ Symbol_Pos.scan_alt_string >> token_range AltString ||
+ scan_verbatim >> token_range Verbatim ||
+ scan_comment >> token_range Comment ||
+ scan_space >> token Space ||
+ scan_malformed >> token Malformed ||
+ Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
+ (Scan.max token_leq
+ (Scan.max token_leq
+ (Scan.literal lex2 >> pair Command)
+ (Scan.literal lex1 >> pair Keyword))
+ (Syntax.scan_longid >> pair LongIdent ||
+ Syntax.scan_id >> pair Ident ||
+ Syntax.scan_var >> pair Var ||
+ Syntax.scan_tid >> pair TypeIdent ||
+ Syntax.scan_tvar >> pair TypeVar ||
+ Syntax.scan_nat >> pair Nat ||
+ scan_symid >> pair SymIdent) >> uncurry token));
+
+fun recover msg =
+ Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
+ >> (single o token (Error msg));
+
+in
+
+fun source' {do_recover} get_lex =
+ Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
+ (Option.map (rpair recover) do_recover);
+
+fun source do_recover get_lex pos src =
+ Symbol_Pos.source pos src
+ |> source' do_recover get_lex;
+
+end;
+
+
+(* read_antiq *)
+
+fun read_antiq lex scan (syms, pos) =
+ let
+ fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
+ "@{" ^ Symbol_Pos.content syms ^ "}");
+
+ val res =
+ Source.of_list syms
+ |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+ |> source_proper
+ |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+ |> Source.exhaust;
+ in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
+
+end;
--- a/src/Pure/ML/ml_context.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Mon May 17 15:11:25 2010 +0200
@@ -112,8 +112,6 @@
local
-structure T = OuterLex;
-
val antiq =
Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
@@ -144,7 +142,8 @@
| expand (Antiquote.Antiq (ss, range)) (scope, background) =
let
val context = Stack.top scope;
- val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
+ val (f, context') =
+ antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
val (decl, background') = f background;
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
in (decl', (Stack.map_top (K context') scope, background')) end
--- a/src/Pure/ROOT.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/ROOT.ML Mon May 17 15:11:25 2010 +0200
@@ -167,7 +167,7 @@
use "Proof/proofchecker.ML";
(*outer syntax*)
-use "Isar/outer_lex.ML";
+use "Isar/token.ML";
use "Isar/keyword.ML";
use "Isar/parse.ML";
use "Isar/parse_value.ML";
@@ -299,6 +299,13 @@
struct
structure OuterKeyword = Keyword;
+
+structure OuterLex =
+struct
+ open Token;
+ type token = T;
+end;
+
structure OuterParse = Parse;
structure OuterSyntax = Outer_Syntax;
structure SpecParse = Parse_Spec;
--- a/src/Pure/Thy/latex.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Thy/latex.ML Mon May 17 15:11:25 2010 +0200
@@ -9,7 +9,7 @@
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
- val output_basic: OuterLex.token -> string
+ val output_basic: Token.T -> string
val output_markup: string -> string -> string
val output_markup_env: string -> string -> string
val output_verbatim: string -> string
@@ -99,24 +99,22 @@
(* token output *)
-structure T = OuterLex;
-
-val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
+val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
fun output_basic tok =
- let val s = T.content_of tok in
+ let val s = Token.content_of tok in
if invisible_token tok then ""
- else if T.is_kind T.Command tok then
+ else if Token.is_kind Token.Command tok then
"\\isacommand{" ^ output_syms s ^ "}"
- else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
+ else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
"\\isakeyword{" ^ output_syms s ^ "}"
- else if T.is_kind T.String tok then
+ else if Token.is_kind Token.String tok then
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
- else if T.is_kind T.AltString tok then
+ else if Token.is_kind Token.AltString tok then
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
- else if T.is_kind T.Verbatim tok then
+ else if Token.is_kind Token.Verbatim tok then
let
- val (txt, pos) = T.source_position_of tok;
+ val (txt, pos) = Token.source_position_of tok;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
--- a/src/Pure/Thy/thy_header.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon May 17 15:11:25 2010 +0200
@@ -6,17 +6,13 @@
signature THY_HEADER =
sig
- val args: OuterLex.token list ->
- (string * string list * (string * bool) list) * OuterLex.token list
+ val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
end;
structure Thy_Header: THY_HEADER =
struct
-structure T = OuterLex;
-
-
(* keywords *)
val headerN = "header";
@@ -58,9 +54,9 @@
let val res =
src
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
- |> T.source_proper
- |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
+ |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
+ |> Token.source_proper
+ |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
|> Source.get_single;
in
(case res of SOME (x, _) => x
--- a/src/Pure/Thy/thy_output.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon May 17 15:11:25 2010 +0200
@@ -24,7 +24,7 @@
val modes: string list Unsynchronized.ref
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
- (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
+ (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
val pretty_text: string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -36,9 +36,6 @@
structure ThyOutput: THY_OUTPUT =
struct
-structure T = OuterLex;
-
-
(** global options **)
val display = Unsynchronized.ref false;
@@ -154,7 +151,7 @@
let
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
| expand (Antiquote.Antiq (ss, (pos, _))) =
- let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
+ let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
options opts (fn () => command src state) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
(Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
@@ -178,7 +175,7 @@
datatype token =
NoToken
- | BasicToken of T.token
+ | BasicToken of Token.T
| MarkupToken of string * (string * Position.T)
| MarkupEnvToken of string * (string * Position.T)
| VerbatimToken of string * Position.T;
@@ -195,10 +192,10 @@
fun basic_token pred (BasicToken tok) = pred tok
| basic_token _ _ = false;
-val improper_token = basic_token (not o T.is_proper);
-val comment_token = basic_token T.is_comment;
-val blank_token = basic_token T.is_blank;
-val newline_token = basic_token T.is_newline;
+val improper_token = basic_token (not o Token.is_proper);
+val comment_token = basic_token Token.is_comment;
+val blank_token = basic_token Token.is_blank;
+val newline_token = basic_token Token.is_newline;
(* command spans *)
@@ -303,19 +300,19 @@
local
val space_proper =
- Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
+ Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
-val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
+val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
val improper = Scan.many is_improper;
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
-val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
-val opt_newline = Scan.option (Scan.one T.is_newline);
+val opt_newline = Scan.option (Scan.one Token.is_newline);
val ignore =
- Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
+ Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
>> pair (d + 1)) ||
- Scan.depend (fn d => Scan.one T.is_end_ignore --|
+ Scan.depend (fn d => Scan.one Token.is_end_ignore --|
(if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
>> pair (d - 1));
@@ -336,18 +333,19 @@
fun markup mark mk flag = Scan.peek (fn d =>
improper |--
- Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
+ Parse.position
+ (Scan.one (Token.is_kind Token.Command andf is_markup mark o Token.content_of)) --
Scan.repeat tag --
Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
- let val name = T.content_of tok
+ let val name = Token.content_of tok
in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
val command = Scan.peek (fn d =>
- Parse.position (Scan.one (T.is_kind T.Command)) --
+ Parse.position (Scan.one (Token.is_kind Token.Command)) --
Scan.repeat tag
>> (fn ((tok, pos), tags) =>
- let val name = T.content_of tok
+ let val name = Token.content_of tok
in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
@@ -367,8 +365,8 @@
(* spans *)
- val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
- val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
+ val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
+ val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
@@ -390,8 +388,8 @@
val spans =
src
- |> Source.filter (not o T.is_semicolon)
- |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
+ |> Source.filter (not o Token.is_semicolon)
+ |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
|> Source.source stopper (Scan.error (Scan.bulk span)) NONE
|> Source.exhaust;
@@ -490,7 +488,7 @@
(* default output *)
-val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
fun maybe_pretty_source pretty src xs =
map pretty xs (*always pretty in order to exhibit errors!*)
--- a/src/Pure/Thy/thy_syntax.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Mon May 17 15:11:25 2010 +0200
@@ -7,18 +7,17 @@
signature THY_SYNTAX =
sig
val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
- (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
+ (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
Source.source) Source.source) Source.source) Source.source
- val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
- val present_token: OuterLex.token -> output
- val report_token: OuterLex.token -> unit
+ val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+ val present_token: Token.T -> output
+ val report_token: Token.T -> unit
datatype span_kind = Command of string | Ignored | Malformed
type span
val span_kind: span -> span_kind
- val span_content: span -> OuterLex.token list
+ val span_content: span -> Token.T list
val span_range: span -> Position.range
- val span_source: (OuterLex.token, 'a) Source.source ->
- (span, (OuterLex.token, 'a) Source.source) Source.source
+ val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
val present_span: span -> output
val report_span: span -> unit
@@ -29,16 +28,13 @@
structure ThySyntax: THY_SYNTAX =
struct
-structure T = OuterLex;
-
-
(** tokens **)
(* parse *)
fun token_source lexs pos src =
Symbol.source {do_recover = true} src
- |> T.source {do_recover = SOME false} (K lexs) pos;
+ |> Token.source {do_recover = SOME false} (K lexs) pos;
fun parse_tokens lexs pos str =
Source.of_string str
@@ -51,33 +47,33 @@
local
val token_kind_markup =
- fn T.Command => (Markup.commandN, [])
- | T.Keyword => (Markup.keywordN, [])
- | T.Ident => Markup.ident
- | T.LongIdent => Markup.ident
- | T.SymIdent => Markup.ident
- | T.Var => Markup.var
- | T.TypeIdent => Markup.tfree
- | T.TypeVar => Markup.tvar
- | T.Nat => Markup.ident
- | T.String => Markup.string
- | T.AltString => Markup.altstring
- | T.Verbatim => Markup.verbatim
- | T.Space => Markup.none
- | T.Comment => Markup.comment
- | T.InternalValue => Markup.none
- | T.Malformed => Markup.malformed
- | T.Error _ => Markup.malformed
- | T.Sync => Markup.control
- | T.EOF => Markup.control;
+ fn Token.Command => (Markup.commandN, [])
+ | Token.Keyword => (Markup.keywordN, [])
+ | Token.Ident => Markup.ident
+ | Token.LongIdent => Markup.ident
+ | Token.SymIdent => Markup.ident
+ | Token.Var => Markup.var
+ | Token.TypeIdent => Markup.tfree
+ | Token.TypeVar => Markup.tvar
+ | Token.Nat => Markup.ident
+ | Token.String => Markup.string
+ | Token.AltString => Markup.altstring
+ | Token.Verbatim => Markup.verbatim
+ | Token.Space => Markup.none
+ | Token.Comment => Markup.comment
+ | Token.InternalValue => Markup.none
+ | Token.Malformed => Markup.malformed
+ | Token.Error _ => Markup.malformed
+ | Token.Sync => Markup.control
+ | Token.EOF => Markup.control;
in
fun present_token tok =
- Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
+ Markup.enclose (token_kind_markup (Token.kind_of tok)) (Output.output (Token.unparse tok));
fun report_token tok =
- Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
+ Position.report (token_kind_markup (Token.kind_of tok)) (Token.position_of tok);
end;
@@ -88,7 +84,7 @@
(* type span *)
datatype span_kind = Command of string | Ignored | Malformed;
-datatype span = Span of span_kind * OuterLex.token list;
+datatype span = Span of span_kind * Token.T list;
fun span_kind (Span (k, _)) = k;
fun span_content (Span (_, toks)) = toks;
@@ -98,8 +94,8 @@
[] => (Position.none, Position.none)
| toks =>
let
- val start_pos = T.position_of (hd toks);
- val end_pos = T.end_position_of (List.last toks);
+ val start_pos = Token.position_of (hd toks);
+ val end_pos = Token.end_position_of (List.last toks);
in (start_pos, end_pos) end);
@@ -107,7 +103,7 @@
local
-val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
+val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
val body =
Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
@@ -120,7 +116,7 @@
in
-fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
+fun span_source src = Source.source Token.stopper (Scan.bulk span) NONE src;
end;
--- a/src/Tools/Code/code_printer.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Mon May 17 15:11:25 2010 +0200
@@ -72,9 +72,9 @@
val parse_infix: ('a -> 'b) -> lrx * int -> string
-> int * ((fixity -> 'b -> Pretty.T)
-> fixity -> 'a list -> Pretty.T)
- val parse_syntax: ('a -> 'b) -> OuterParse.token list
+ val parse_syntax: ('a -> 'b) -> Token.T list
-> (int * ((fixity -> 'b -> Pretty.T)
- -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
+ -> fixity -> 'a list -> Pretty.T)) option * Token.T list
val simple_const_syntax: simple_const_syntax -> proto_const_syntax
val activate_const_syntax: theory -> literals
-> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
--- a/src/Tools/Code/code_target.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Tools/Code/code_target.ML Mon May 17 15:11:25 2010 +0200
@@ -19,14 +19,13 @@
type destination
type serialization
- val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
- -> OuterLex.token list -> 'a
+ val parse_args: 'a parser -> Token.T list -> 'a
val stmt_names_of_destination: destination -> string list
val mk_serialization: string -> ('a -> unit) option
-> (Path.T option -> 'a -> unit)
-> ('a -> string * string option list)
-> 'a -> serialization
- val serialize: theory -> string -> int option -> string option -> OuterLex.token list
+ val serialize: theory -> string -> int option -> string option -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
val serialize_custom: theory -> string * (serializer * literals)
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
@@ -105,7 +104,7 @@
type serializer =
string option (*module name*)
- -> OuterLex.token list (*arguments*)
+ -> Token.T list (*arguments*)
-> (string -> string) (*labelled_name*)
-> string list (*reserved symbols*)
-> (string * Pretty.T) list (*includes*)
@@ -498,7 +497,7 @@
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
- case Scan.read OuterLex.stopper f args
+ case Scan.read Token.stopper f args
of SOME x => x
| NONE => error "Bad serializer arguments";
@@ -575,8 +574,8 @@
K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
fun shell_command thyname cmd = Toplevel.program (fn _ =>
- (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
- ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
+ (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
+ ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
of SOME f => (writeln "Now generating code..."; f (theory thyname))
| NONE => error ("Bad directive " ^ quote cmd)))
handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
--- a/src/Tools/WWW_Find/find_theorems.ML Mon May 17 15:05:32 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Mon May 17 15:11:25 2010 +0200
@@ -195,7 +195,7 @@
query
|> (fn s => s ^ ";")
|> OuterSyntax.scan Position.start
- |> filter OuterLex.is_proper
+ |> filter Token.is_proper
|> Scan.error parse_query
|> fst;