src/Pure/PIDE/resources.ML
changeset 57905 c0c5652e796e
parent 56803 d3cc56ca54c9
child 57918 f5d73caba4e5
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Aug 11 22:59:38 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 00:08:32 2014 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4  fun excursion master_dir last_timing init elements =
     1.5    let
     1.6      fun prepare_span span =
     1.7 -      Thy_Syntax.span_content span
     1.8 +      Command_Span.content span
     1.9        |> Command.read init master_dir []
    1.10        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    1.11  
    1.12 @@ -157,8 +157,8 @@
    1.13      val _ = Thy_Header.define_keywords header;
    1.14  
    1.15      val lexs = Keyword.get_lexicons ();
    1.16 -    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
    1.17 -    val spans = Thy_Syntax.parse_spans toks;
    1.18 +    val toks = Outer_Syntax.parse_tokens lexs text_pos text;
    1.19 +    val spans = Outer_Syntax.parse_spans toks;
    1.20      val elements = Thy_Syntax.parse_elements spans;
    1.21  
    1.22      fun init () =