1.1 --- a/test/Pure/Isar/Test_Parse_Term.thy Thu Mar 18 13:56:45 2021 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,95 +0,0 @@
1.4 -(* experiments on scanning and parsing
1.5 - following Stefan Berghofers presentation
1.6 - at the Isabelle Developer Workshop 2010 *)
1.7 -
1.8 -theory Test_Parse_Term
1.9 -imports Main
1.10 -begin
1.11 -
1.12 -section \<open>parse following Stefan Berghofer at Isabelle Developer Workshop 2010\<close>
1.13 -ML \<open>
1.14 -fun filtered_input str =
1.15 - filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
1.16 -fun parse p str = Scan.finite Token.stopper p (filtered_input str);
1.17 -\<close>
1.18 -
1.19 -text \<open>should not Parse.term repeat until a non-term token is reached ?
1.20 - ######################\" IS REQUIRED \"#######################\<close>
1.21 -ML \<open>
1.22 -parse Parse.term "\"xxx +++ 111\" end";
1.23 -(*val it =
1.24 - ("\^E\^Ftoken\^Exxx +++ 111\^E\^F\^E", [Token (("end", ({}, {})), (Command, "end"), Slot)])
1.25 - : string * Token.T list*)
1.26 -parse (Scan.repeat Parse.term) "\"xxx +++ 111\" end";
1.27 -(*val it =
1.28 - (["\^E\^Ftoken\^Exxx +++ 111\^E\^F\^E"], [Token (("end", ({}, {})), (Command, "end"), Slot)])
1.29 - : string list * Token.T list*)
1.30 -\<close>
1.31 -
1.32 -text \<open>Parse.term stops at "Keyword" of outer syntax ?!?
1.33 - Should not be parsed according to inner xyntax ?\<close>
1.34 -ML \<open>
1.35 -parse Parse.term "\"xxx + 111\" end";
1.36 -(*val it = ("\^E\^Ftoken\^Exxx + 111\^E\^F\^E", [Token (("end", ({}, {})), (Command, "end"), Slot)])
1.37 - : string * Token.T list*)
1.38 -parse Parse.term "\"aaa\" \"xxx +++ (111)\" end";
1.39 -(*val it =
1.40 - ("\^E\^Ftoken\^Eaaa\^E\^F\^E",
1.41 - [Token (("xxx +++ (111)", ({}, {})), (..., "xxx +++ (111)"), Slot),
1.42 - Token (("end", ({}, {})), (Command, "end"), Slot)])
1.43 - : string * Token.T list*)
1.44 -\<close>
1.45 -
1.46 -
1.47 -section \<open>decompose term\<close>
1.48 -ML \<open>
1.49 -(*========== inhibit exn 110314 ================================================
1.50 -"---from src/Pure/Isar/token.ML ----------------------------------------------";
1.51 -datatype value =
1.52 - Text of string | Typ of typ | Term of term | Fact of thm list | Attribute of morphism -> attribute;
1.53 -datatype slot =
1.54 - Slot | Value of value option | Assignable of value option Unsynchronized.ref;
1.55 -datatype kind =
1.56 - Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
1.57 - Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
1.58 - Malformed | Error of string | Sync | EOF;
1.59 -datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
1.60 - fun source_of (Token ((source, (pos, _)), _, _)) =
1.61 - YXML.string_of (XML.Elem (Markup.tokenN,
1.62 - Position.properties_of pos, [XML.Text source]));
1.63 - (*fn : T -> string*)
1.64 -"---from src/Pure/General/scan.ML --------------------------------------------------------------------------------";
1.65 - fun ahead scan xs = (fst (scan xs), xs);
1.66 - (*fn : ('a -> 'b * 'c) -> 'a -> 'b * 'a*)
1.67 -"---from src/Pure/Isar/parse.ML ----------------------------------------------------------------------------------";
1.68 - (*fn : Token.T list -> string * Token.T list*)
1.69 - fun fail_with s = Scan.fail_with
1.70 - (fn [] => s ^ " expected (past end-of-file!)"
1.71 - | (tok :: _) =>
1.72 - (case Token.text_of tok of
1.73 - (txt, "") =>
1.74 - s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok
1.75 - ^ " was found"
1.76 - | (txt1, txt2) =>
1.77 - s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok
1.78 - ^ " was found:\n" ^ txt2));
1.79 - (*fn : string -> Token.T list -> 'a*)
1.80 - fun RESET_VALUE atom = Scan.ahead (Scan.one (K true)) --
1.81 - atom >> (fn (arg, x) => (Token.assign NONE arg; x));
1.82 - (*fn : (Token.T list -> 'a * 'b) -> Token.T list -> 'a * 'b*)
1.83 - val not_eof = RESET_VALUE (Scan.one Token.not_eof);
1.84 - (*fn : Token.T list -> Token.T * Token.T list*)
1.85 - fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
1.86 - (*fn : (Token.T list -> 'a * 'b) -> Token.T list -> string * Token.T list*)
1.87 - fun group s scan = scan || fail_with s;
1.88 - (*fn : string -> (Token.T list -> 'a) -> Token.T list -> 'a*)
1.89 - val trm = Parse.short_ident || Parse.long_ident || Parse.sym_ident ||
1.90 - Parse.term_var || Parse.number || Parse.string;
1.91 - val term_group = group "term" trm;
1.92 - (*fn : Token.T list -> string * Token.T list*)
1.93 -val term = inner_syntax term_group;
1.94 -(*fn : Token.T list -> string * Token.T list*)
1.95 -============ inhibit exn 110314 ==============================================*)
1.96 -\<close>
1.97 -
1.98 -end
1.99 \ No newline at end of file