src/Pure/Isar/outer_syntax.ML
changeset 7755 01e3d545ced8
parent 7750 e63416829538
child 7768 b106e4af1301
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Oct 06 18:11:37 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Oct 06 18:12:05 1999 +0200
     1.3 @@ -333,14 +333,14 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val scan_markup =
     1.8 -  Scan.one T.not_eof :-- (fn tok =>
     1.9 -    if T.is_kind T.Command tok andalso is_markup (T.val_of tok) then
    1.10 -      (Scan.any (not o T.is_proper) |-- P.text) >> Some
    1.11 -    else Scan.succeed None);
    1.12 +val improper = Scan.any (not o T.is_proper);
    1.13 +val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    1.14  
    1.15 -fun invisible_token (tok, arg) =
    1.16 -  is_none arg andalso T.keyword_with (equal ";") tok orelse T.is_kind T.Comment tok;
    1.17 +val present_token =
    1.18 +  improper |-- markup -- (improper |-- P.text --| (improper -- Scan.option semicolon -- improper))
    1.19 +    >> Present.markup_token ||
    1.20 +  (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
    1.21 +  Scan.one T.not_eof >> Present.basic_token;
    1.22  
    1.23  in
    1.24  
    1.25 @@ -348,9 +348,8 @@
    1.26  
    1.27  fun present_toks text pos () =
    1.28    token_source (Source.of_list (Library.untabify text), pos)
    1.29 -  |> Source.source T.stopper (Scan.bulk scan_markup) None
    1.30 -  |> Source.exhaust
    1.31 -  |> filter_out invisible_token;
    1.32 +  |> Source.source T.stopper (Scan.bulk present_token) None
    1.33 +  |> Source.exhaust;
    1.34  
    1.35  fun present_text text () =
    1.36    Source.exhaust (Symbol.source false (Source.of_list (Library.untabify text)));