src/Pure/PIDE/resources.ML
changeset 58903 38c72f5f6c2e
parent 58862 63a16e98cc14
child 58904 f49c4f883c58
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Nov 05 20:05:32 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Wed Nov 05 20:20:57 2014 +0100
     1.3 @@ -148,8 +148,7 @@
     1.4      val {name = (name, _), ...} = header;
     1.5      val _ = Thy_Header.define_keywords header;
     1.6  
     1.7 -    val lexs = Keyword.get_lexicons ();
     1.8 -    val toks = Outer_Syntax.scan lexs text_pos text;
     1.9 +    val toks = Outer_Syntax.scan (Keyword.get_keywords ()) text_pos text;
    1.10      val spans = Outer_Syntax.parse_spans toks;
    1.11      val elements = Thy_Syntax.parse_elements spans;
    1.12  
    1.13 @@ -165,13 +164,13 @@
    1.14      fun present () =
    1.15        let
    1.16          val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    1.17 -        val ((minor, _), syntax) = Outer_Syntax.get_syntax ();
    1.18 +        val (keywords, syntax) = Outer_Syntax.get_syntax ();
    1.19        in
    1.20          if exists (Toplevel.is_skipped_proof o #2) res then
    1.21            warning ("Cannot present theory with skipped proofs: " ^ quote name)
    1.22          else
    1.23            let val tex_source =
    1.24 -            Thy_Output.present_thy minor Keyword.command_tags
    1.25 +            Thy_Output.present_thy keywords Keyword.command_tags
    1.26                (Outer_Syntax.is_markup syntax) res toks
    1.27              |> Buffer.content;
    1.28            in if document then Present.theory_output name tex_source else () end