let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in
let whelp_query_RE = Pcre.regexp
- "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$"
+ "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$"
in
let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in
let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
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);
| `NRef nref -> self#_loadNReference nref
| `Univs uri -> self#_loadUnivs uri
| `Whelp (query, results) ->
- set_whelp_query query;
self#_loadList (List.map (fun r -> "obj",
UriManager.string_of_uri r) results));
self#setEntry entry
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
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