equal
deleted
inserted
replaced
1 chapter \<open>experiments on scanning and parsing |
1 chapter \<open>experiments on scanning and parsing |
2 following Stefan Berghofers presentation |
2 following Stefan Berghofers presentation |
3 at the Isabelle Developer Workshop 2010 |
3 at the Isabelle Developer Workshop 2010 |
4 ... broken Isabelle2014-->Isabelle2015, not pursued anymore and thus dropped\<close> |
4 ... broken Isabelle2014-->Isabelle2015, not pursued anymore and thus dropped\<close> |
5 |
5 |
6 theory Test_Parsers |
6 theory Test_Parsers |
7 imports Main |
7 imports Main |
8 begin |
8 begin |
9 |
9 |
10 text \<open>parse following Stefan Berghofer at Isabelle Developer Workshop 2010\<close> |
10 text \<open>parse following Stefan Berghofer at Isabelle Developer Workshop 2010\<close> |
11 ML \<open> |
11 ML \<open> |
12 fun filtered_input str = |
12 fun filtered_input str = |
13 filter Token.is_proper (Outer_Syntax.scan Position.none str); |
13 filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) |
14 fun parse p str = Scan.finite Token.stopper p (filtered_input str); |
14 fun parse p str = Scan.finite Token.stopper p (filtered_input str); |
|
15 \<close> ML \<open> |
|
16 \<close> ML \<open> |
|
17 \<close> ML \<open> |
15 \<close> |
18 \<close> |
16 |
19 |
17 section \<open>scanner combinators from src/Pure/General/scan.ML\<close> |
20 section \<open>scanner combinators from src/Pure/General/scan.ML\<close> |
18 text \<open>ATTENTION, there are several similar definitions: |
21 text \<open>ATTENTION, there are several similar definitions: |
19 src> grep -r 'infix ' * | grep '\-\- ' | less |
22 src> grep -r 'infix ' * | grep '\-\- ' | less |