src/Pure/PIDE/resources.ML
changeset 61381 ddca85598c65
parent 61379 c57820ceead3
child 63669 256fc20716f2
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Oct 09 21:20:43 2015 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Oct 10 16:21:34 2015 +0200
     1.3 @@ -17,8 +17,9 @@
     1.4    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     1.5    val loaded_files_current: theory -> bool
     1.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     1.7 -  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
     1.8 -    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
     1.9 +  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time option) -> int ->
    1.10 +    Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
    1.11 +    theory * (unit -> unit) * int
    1.12  end;
    1.13  
    1.14  structure Resources: RESOURCES =
    1.15 @@ -145,7 +146,7 @@
    1.16      val thy = Toplevel.end_theory end_pos end_state;
    1.17    in (results, thy) end;
    1.18  
    1.19 -fun load_thy document last_timing update_time master_dir header text_pos text parents =
    1.20 +fun load_thy document symbols last_timing update_time master_dir header text_pos text parents =
    1.21    let
    1.22      val (name, _) = #name header;
    1.23      val keywords =
    1.24 @@ -159,7 +160,7 @@
    1.25      fun init () =
    1.26        begin_theory master_dir header parents
    1.27        |> Present.begin_theory update_time
    1.28 -        (fn () => implode (map (HTML.present_span keywords) spans));
    1.29 +        (fn () => implode (map (HTML.present_span symbols keywords) spans));
    1.30  
    1.31      val (results, thy) =
    1.32        cond_timeit true ("theory " ^ quote name)