# HG changeset patch # User wenzelm # Date 1274101885 -7200 # Node ID f5417836dbead656bee2e399b8b87902bb9d1cdb # Parent ad5313f1bd30418e8458c27d75da3e3ce8d44af6 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T; diff -r ad5313f1bd30 -r f5417836dbea NEWS --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/HOL/Import/import_syntax.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/Pure/IsaMakefile --- 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 \ diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/args.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; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/attrib.ML --- 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 *) diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/method.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/outer_lex.ML --- 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 "" o Text; -val mk_typ = mk_value "" o Typ; -val mk_term = mk_value "" o Term; -val mk_fact = mk_value "" o Fact; -val mk_attribute = mk_value "" 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; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/outer_syntax.ML --- 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; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/parse.ML --- 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 = $$$ ";"; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/rule_insts.ML --- 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; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Isar/token.ML --- /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 "" o Text; +val mk_typ = mk_value "" o Typ; +val mk_term = mk_value "" o Term; +val mk_fact = mk_value "" o Fact; +val mk_attribute = mk_value "" 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; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/ML/ml_context.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/Pure/ROOT.ML --- 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; diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Thy/latex.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Thy/thy_header.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Thy/thy_output.ML --- 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!*) diff -r ad5313f1bd30 -r f5417836dbea src/Pure/Thy/thy_syntax.ML --- 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; diff -r ad5313f1bd30 -r f5417836dbea src/Tools/Code/code_printer.ML --- 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 diff -r ad5313f1bd30 -r f5417836dbea src/Tools/Code/code_target.ML --- 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; diff -r ad5313f1bd30 -r f5417836dbea src/Tools/WWW_Find/find_theorems.ML --- 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;