X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=71e7cb55334540bbbf61640ecf5b2f2d4b5fcec7;hb=ef98db5ff416ef53004e57cc054e28abd1bf871e;hp=e76c659a4cb42ab194754060e36ca392fb76192e;hpb=ad8d37cce3b39565861014d870b91b1add0ec0e3;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index e76c659a4..71e7cb553 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -981,7 +981,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) combo#set_active (aux 0 queries); in let searchText = - GSourceView.source_view ~auto_indent:false ~editable:false () + GSourceView2.source_view ~auto_indent:false ~editable:false () in let _ = win#scrolledwinContent#add (searchText :> GObj.widget); @@ -1476,7 +1476,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadTermNCic term m s c = let d = 0 in - let m = (0,(None,c,term))::m in + let m = (0,([],c,term))::m in let status = (MatitaScript.current ())#grafite_status in mathView#nload_sequent status m s d; self#_showMath @@ -1642,12 +1642,22 @@ let mathViewer () = x ^ ".label.png") filenames in + let rec div2 = function + | [] -> [] + | [x] -> [[x]] + | x::y::tl -> [x;y] :: div2 tl + in + let items = div2 items in ignore(Sys.command (Printf.sprintf - "convert %s +append %s" - (String.concat (" '(' -gravity center -size 10x10 xc: ')' ") items) + "convert %s -append %s" + (String.concat "" + (List.map (fun items -> + Printf.sprintf " '(' %s +append ')' " + (String.concat + (" '(' -gravity center -size 10x10 xc: ')' ") items)) items)) (Filename.quote (ofn ^ ".png")))); List.iter (fun x,_ -> Sys.remove x) filenames; - List.iter Sys.remove items; + List.iter Sys.remove (List.flatten items); w#destroy (); end