src/Pure/Isar/outer_syntax.ML
changeset 12876 a70df1e5bf10
parent 10749 afdb47b97317
child 12943 1db24da0537b
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Feb 12 20:25:58 2002 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Feb 12 20:28:27 2002 +0100
     1.3 @@ -228,20 +228,19 @@
     1.4  
     1.5  (* basic sources *)
     1.6  
     1.7 -fun token_source (src, pos) =
     1.8 -  src
     1.9 -  |> Symbol.source false
    1.10 -  |> T.source false (K (get_lexicons ())) pos;
    1.11 -
    1.12  fun toplevel_source term do_recover cmd src =
    1.13    let
    1.14      val no_terminator =
    1.15        Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
    1.16 -    val recover = Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None];
    1.17 +    fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]) x;
    1.18    in
    1.19      src
    1.20 +    |> T.source_proper
    1.21      |> Source.source T.stopper
    1.22 -      (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
    1.23 +      (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some))
    1.24 +      (if do_recover then Some recover else None)
    1.25 +    |> Source.mapfilter I
    1.26 +    |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
    1.27        (if do_recover then Some recover else None)
    1.28      |> Source.mapfilter I
    1.29    end;
    1.30 @@ -254,7 +253,6 @@
    1.31    |> Symbol.source true
    1.32    |> T.source true get_lexicons
    1.33      (if no_pos then Position.none else Position.line_name 1 "stdin")
    1.34 -  |> T.source_proper
    1.35    |> toplevel_source term true get_parser;
    1.36  
    1.37  
    1.38 @@ -294,7 +292,6 @@
    1.39  
    1.40  fun parse_thy src =
    1.41    src
    1.42 -  |> T.source_proper
    1.43    |> toplevel_source false false (K (get_parser ()))
    1.44    |> Source.exhaust;
    1.45  
    1.46 @@ -311,7 +308,10 @@
    1.47        Present.old_symbol_source name present_text)   (*note: text presented twice*)
    1.48      else
    1.49        let
    1.50 -        val tok_src = Source.exhausted (token_source (text_src, pos));
    1.51 +        val tok_src = text_src
    1.52 +          |> Symbol.source false
    1.53 +          |> T.source false (K (get_lexicons ())) pos
    1.54 +          |> Source.exhausted;
    1.55          val out = Toplevel.excursion_result
    1.56            (IsarOutput.parse_thy markup (#1 (get_lexicons ()))
    1.57              (parse_thy tok_src) tok_src);