src/Pure/PIDE/resources.ML
changeset 58928 23d0ffd48006
parent 58923 cb9b69cca999
child 58934 385a4cc7426f
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Nov 07 16:22:25 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Nov 07 16:36:55 2014 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4      (case Token.get_files tok of
     1.5        [] =>
     1.6          let
     1.7 -          val keywords = Keyword.get_keywords ();
     1.8 +          val keywords = Thy_Header.get_keywords thy;
     1.9            val master_dir = master_directory thy;
    1.10            val pos = Token.pos_of tok;
    1.11            val src_paths = Keyword.command_files keywords cmd (Path.explode name);
    1.12 @@ -122,18 +122,18 @@
    1.13  fun begin_theory master_dir {name, imports, keywords} parents =
    1.14    Theory.begin_theory name parents
    1.15    |> put_deps master_dir imports
    1.16 -  |> fold Thy_Header.declare_keyword keywords;
    1.17 +  |> Thy_Header.add_keywords keywords;
    1.18  
    1.19  fun excursion keywords master_dir last_timing init elements =
    1.20    let
    1.21 -    fun prepare_span span =
    1.22 +    fun prepare_span st span =
    1.23        Command_Span.content span
    1.24 -      |> Command.read keywords master_dir init []
    1.25 +      |> Command.read (Command.read_thy st) master_dir init []
    1.26        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    1.27  
    1.28      fun element_result span_elem (st, _) =
    1.29        let
    1.30 -        val elem = Thy_Syntax.map_element prepare_span span_elem;
    1.31 +        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
    1.32          val (results, st') = Toplevel.element_result keywords elem st;
    1.33          val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
    1.34        in (results, (st', pos')) end;
    1.35 @@ -147,8 +147,9 @@
    1.36  fun load_thy document last_timing update_time master_dir header text_pos text parents =
    1.37    let
    1.38      val (name, _) = #name header;
    1.39 -    val _ = Thy_Header.define_keywords (#keywords header);
    1.40 -    val keywords = Keyword.get_keywords ();
    1.41 +    val keywords =
    1.42 +      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
    1.43 +        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
    1.44  
    1.45      val toks = Outer_Syntax.scan keywords text_pos text;
    1.46      val spans = Outer_Syntax.parse_spans toks;
    1.47 @@ -166,14 +167,11 @@
    1.48      fun present () =
    1.49        let
    1.50          val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    1.51 -        val (keywords, syntax) = Outer_Syntax.get_syntax ();
    1.52        in
    1.53          if exists (Toplevel.is_skipped_proof o #2) res then
    1.54            warning ("Cannot present theory with skipped proofs: " ^ quote name)
    1.55          else
    1.56 -          let val tex_source =
    1.57 -            Thy_Output.present_thy keywords (Outer_Syntax.is_markup syntax) res toks
    1.58 -            |> Buffer.content;
    1.59 +          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
    1.60            in if document then Present.theory_output name tex_source else () end
    1.61        end;
    1.62