1.1 --- a/src/Pure/PIDE/document.ML	Sun Feb 24 14:14:07 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Feb 24 17:29:55 2013 +0100
     1.3 @@ -268,9 +268,8 @@
     1.4        val id_string = print_id id;
     1.5        val span = Lazy.lazy (fn () =>
     1.6          Position.setmp_thread_data (Position.id_only id_string)
     1.7 -          (fn () =>
     1.8 -            Thy_Syntax.parse_tokens
     1.9 -              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
    1.10 +          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
    1.11 +            ());
    1.12        val _ =
    1.13          Position.setmp_thread_data (Position.id_only id_string)
    1.14            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    1.15 @@ -453,7 +452,7 @@
    1.16            (fn () =>
    1.17              let
    1.18                val tr =
    1.19 -                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    1.20 +                Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
    1.21                  |> modify_init
    1.22                  |> Toplevel.put_id exec_id'_string;
    1.23                val cmts = Outer_Syntax.span_cmts span;