src/Pure/Isar/outer_syntax.ML
changeset 8583 34c4847fd8c1
parent 8209 4816ba139574
child 8652 39a695b0b1d7
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Mar 26 20:12:28 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 26 20:13:53 2000 +0200
     1.3 @@ -343,24 +343,36 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val indent_prop = Scan.one T.is_indent -- Scan.one T.is_proper;
     1.8 -val improp = Scan.unless indent_prop (Scan.one (not o T.is_proper));
     1.9 -val improper_keep_indent = Scan.repeat improp;
    1.10 +val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
    1.11 +val improper = Scan.any is_improper;
    1.12  
    1.13 -val improper = Scan.any (not o T.is_proper);
    1.14 +val improper_keep_indent = Scan.repeat
    1.15 +  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
    1.16  
    1.17  val improper_end =
    1.18    (improper -- semicolon) |-- improper_keep_indent ||
    1.19    improper_keep_indent;
    1.20  
    1.21 +
    1.22 +val ignore =
    1.23 +  Scan.depend (fn d => Scan.one T.is_begin_ignore >> pair (d + 1)) ||
    1.24 +  Scan.depend (fn 0 => Scan.fail | d => Scan.one T.is_end_ignore >> pair (d - 1)) ||
    1.25 +  Scan.lift (Scan.one (OuterLex.not_eof andf (not o OuterLex.is_end_ignore)));
    1.26 +
    1.27 +val ignore_stuff =
    1.28 +  Scan.one T.is_begin_ignore |--
    1.29 +    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore);
    1.30 +
    1.31  val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    1.32  val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
    1.33  
    1.34  val present_token =
    1.35 -  improper |-- markup -- (improper |-- P.text --| improper_end) >> Present.markup_token ||
    1.36 -  (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
    1.37 -  (improper -- verbatim -- improper) |-- P.text --| improper_end >> Present.verbatim_token ||
    1.38 -  Scan.one T.not_eof >> Present.basic_token;
    1.39 +  ignore_stuff >> K None ||
    1.40 +  (improper |-- markup -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_token ||
    1.41 +    (P.$$$ "--" >> K "cmt") -- P.!!!! (improper |-- P.text) >> Present.markup_token ||
    1.42 +    (improper -- verbatim) |-- P.!!!! (improper |-- P.text --| improper_end)
    1.43 +      >> Present.verbatim_token ||
    1.44 +    Scan.one T.not_eof >> Present.basic_token) >> Some;
    1.45  
    1.46  in
    1.47  
    1.48 @@ -368,7 +380,8 @@
    1.49  
    1.50  fun present_toks text pos () =
    1.51    token_source (Source.of_list (Library.untabify text), pos)
    1.52 -  |> Source.source T.stopper (Scan.bulk present_token) None
    1.53 +  |> Source.source T.stopper (Scan.bulk (Scan.error present_token)) None
    1.54 +  |> Source.mapfilter I
    1.55    |> Source.exhaust;
    1.56  
    1.57  fun present_text text () =