+let eval_with_engine guistuff status user_goal parsed_text st =
+ try
+ eval_with_engine guistuff status user_goal parsed_text st
+ with
+ MatitaEngine.UnableToInclude what as exc ->
+ let compile_needed_and_go_on d =
+ let root = MatitamakeLib.root_for_development d in
+ let target = root ^ "/" ^ what in
+ let refresh_cb () =
+ while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+ in
+ if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
+ raise exc
+ else
+ eval_with_engine guistuff status user_goal parsed_text st
+ in
+ let do_nothing () = [], 0 in
+ let handle_with_devel d =
+ let name = MatitamakeLib.name_for_development d in
+ let title = "Unable to include " ^ what in
+ let message =
+ what ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
+ "<i>Should I compile it and Its dependencies?</i>"
+ in
+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES -> compile_needed_and_go_on d
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing ())
+ in
+ let handle_withoud_devel filename =
+ let title = "Unable to include " ^ what in
+ let message =
+ what ^ " is <b>not</b> handled by a development.\n" ^
+ "All dependencies are authomatically solved for a development.\n\n" ^
+ "<i>Do you want to set up a development?</i>"
+ in
+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES ->
+ (match filename with
+ | Some f ->
+ guistuff.develcreator ~containing:(Some (Filename.dirname f))
+ | None -> guistuff.develcreator ~containing:None);
+ do_nothing ()
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing())
+ in
+ match guistuff.filenamedata with
+ | None,None -> handle_withoud_devel None
+ | None,Some d -> handle_with_devel d
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> handle_withoud_devel (Some f)
+ | Some d -> handle_with_devel d
+;;
+