matita now includes compiling. if the file is not compiled it compiles it,

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 7fe9cdedb5357e94917da928a74ddb9de96ba3e4..b2f509b25ca036f2b16ab5003b1a10e6c721f867 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -58,6 +58,7 @@ class console ~(buffer: GText.buffer) () =
     method clear () =
       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
     method log_callback (tag: HLog.log_tag) s =
+      let s = Pcre.replace ~pat:"\e\\[0;3.m([^\e]+)\e\\[0m" ~templ:"$1" s in
       match tag with
       | `Debug -> self#debug (s ^ "\n")
       | `Error -> self#error (s ^ "\n")
@@ -1155,6 +1156,7 @@ class gui () =
       else
         begin
           script#assignFileName (Some file);
+          let file = script#filename in
           let content =
            if Sys.file_exists file then file
            else BuildTimeConf.script_template