--- a/src/Pure/PIDE/session.ML Sun Nov 15 16:51:58 2020 +0000
+++ b/src/Pure/PIDE/session.ML Mon Nov 16 13:11:15 2020 +0100
@@ -9,7 +9,7 @@
val get_name: unit -> string
val welcome: unit -> string
val get_keywords: unit -> Keyword.keywords
- val init: HTML.symbols -> bool -> Path.T -> string list -> string -> string * string -> bool -> unit
+ val init: bool -> Path.T -> string list -> string -> string * string -> bool -> unit
val shutdown: unit -> unit
val finish: unit -> unit
end;
@@ -45,12 +45,12 @@
(* init *)
-fun init symbols info info_path documents parent (chapter, name) verbose =
+fun init info info_path documents parent (chapter, name) verbose =
(Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
if parent_name <> parent orelse not parent_finished then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else ({chapter = chapter, name = name}, false));
- Present.init symbols info info_path documents (chapter, name) verbose);
+ Present.init info info_path documents (chapter, name) verbose);
(* finish *)