src/Pure/Thy/thy_output.ML
changeset 58861 5ff61774df11
parent 58741 6e7b009e6d94
child 58864 505a8150368a
equal deleted inserted replaced
58860:fee7cfa69c50 58861:5ff61774df11
   411         Scan.option (newline >> (single o snd))
   411         Scan.option (newline >> (single o snd))
   412       >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
   412       >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
   413           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
   413           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
   414 
   414 
   415     val spans = toks
   415     val spans = toks
   416       |> filter_out Token.is_semicolon
       
   417       |> take_suffix Token.is_space |> #1
   416       |> take_suffix Token.is_space |> #1
   418       |> Source.of_list
   417       |> Source.of_list
   419       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
   418       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
   420       |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
   419       |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
   421       |> Source.exhaust;
   420       |> Source.exhaust;