src/Pure/Thy/thy_load.ML
changeset 44478 4fdb1009a370
parent 44353 02f286491568
child 46737 09ab89658a5d
equal deleted inserted replaced
44477:086bb1083552 44478:4fdb1009a370
   173 
   173 
   174     val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
   174     val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
   175     val spans = Source.exhaust (Thy_Syntax.span_source toks);
   175     val spans = Source.exhaust (Thy_Syntax.span_source toks);
   176     val elements =
   176     val elements =
   177       Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
   177       Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
   178       |> maps (Outer_Syntax.prepare_element outer_syntax init);
   178       |> maps (Outer_Syntax.read_element outer_syntax init);
   179 
   179 
   180     val _ = Present.theory_source name
   180     val _ = Present.theory_source name
   181       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
   181       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
   182 
   182 
   183     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
   183     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();