X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaScript.ml;h=6d703b556b3706abeb94281d1c44a0af0dd1d3a4;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=af3cdf12eb15c7a1381e3e3af84f295838974b20;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml index af3cdf12e..6d703b556 100644 --- a/matitaB/matita/matitaScript.ml +++ b/matitaB/matita/matitaScript.ml @@ -65,30 +65,23 @@ let first_line s = String.sub s 0 nl_pos with Not_found -> s +(* WR: skipped_txt, nonskipped_txt servono ancora? + * (ora non abbiamo più gli alias e il codice sembra più complicato + * del necessario) + * (rif. nota 11/05/11 *) let eval_with_engine include_paths status skipped_txt nonskipped_txt st = let parsed_text_length = - String.length skipped_txt + String.length nonskipped_txt + String.length skipped_txt + String.length nonskipped_txt in let text = skipped_txt ^ nonskipped_txt in let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in - let enriched_history_fragment = + let new_status = MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") status (text,prefix_len,st) in - let enriched_history_fragment = List.rev enriched_history_fragment in - (* really fragile *) - let res,_ = - List.fold_left - (fun (acc, to_prepend) (status,alias) -> - match alias with - | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" - | Some (k,value) -> - let newtxt = GrafiteAstPp.pp_alias value in - (status,to_prepend ^ newtxt ^ "\n")::acc, "") - ([],skipped_txt) enriched_history_fragment - in + let res = new_status,skipped_txt ^ nonskipped_txt in res,"",parsed_text_length ;; @@ -106,7 +99,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse List.filter (fun x,_ -> List.mem x selected) menv in CicMathView.screenshot status sequents menv subst name; - [status, parsed_text], "", parsed_text_length + (status, parsed_text), "", parsed_text_length | TA.NCheck (_,t) -> let status = script#status in let _,_,menv,subst,_ = status#obj in @@ -126,13 +119,13 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse (* XXX use the metasenv, if possible *) in MatitaMathView.cicBrowser (Some (`NCic (t,ctx,m,s))); - [status, parsed_text], "", parsed_text_length + (status, parsed_text), "", parsed_text_length | TA.NIntroGuess _loc -> let names_ref = ref [] in let s = NTactics.intros_tac ~names_ref [] script#status in let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in - [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length + (s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"), "", parsed_text_length | TA.NAutoInteractive (_loc, (None,a)) -> let trace_ref = ref [] in let s = NnAuto.auto_tac ~params:(None,a) ~trace_ref script#status in @@ -153,7 +146,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse in let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in - [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length + (s, nl ^ trace ^ thms ^ ";"), "", parsed_text_length | TA.NAutoInteractive (_, (Some _,_)) -> assert false let rec eval_executable include_paths (buffer : GText.buffer) @@ -166,7 +159,7 @@ status unparsed_text skipped_txt nonskipped_txt script ex loc eval_with_engine include_paths status skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with - MatitaTypes.Cancel -> [], "", 0 + MatitaTypes.Cancel -> (status,skipped_txt), "", 0 | GrafiteEngine.NMacro (_loc,macro) -> eval_nmacro include_paths buffer status unparsed_text (skipped_txt ^ nonskipped_txt) script macro @@ -187,12 +180,12 @@ and eval_statement include_paths (buffer : GText.buffer) status script | `Ast (st, text) -> st, text in let text_of_loc floc = - let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let nonskipped_txt,_ = HExtlib.utf8_parsed_text unparsed_text floc in let start, stop = HExtlib.loc_of_floc floc in let floc = HExtlib.floc_of_loc (0, start) in - let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let skipped_txt,_ = HExtlib.utf8_parsed_text unparsed_text floc in let floc = HExtlib.floc_of_loc (0, stop) in - let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let txt,len = HExtlib.utf8_parsed_text unparsed_text floc in txt,nonskipped_txt,skipped_txt,len in match st with @@ -216,16 +209,14 @@ and eval_statement include_paths (buffer : GText.buffer) status script HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn - | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> + (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> raise (MultiPassDisambiguator.DisambiguationError - (offset+parsed_text_length, errorll)) + (offset+parsed_text_length, errorll)) *) in assert (text=""); (* no macros inside comments, please! *) - (match s with - | (statuses,text)::tl -> - (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len - | [] -> [], "", 0) + let st,text = s in + (st,parsed_text ^ text),"",parsed_text_length + len let fresh_script_id = let i = ref 0 in @@ -254,7 +245,8 @@ let source_buffer = source_view#source_buffer in let similarsymbols_tag_name = "similarsymbolos" in let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = - let status = new MatitaEngine.status baseuri in +(* FIXME : currently hard coded to single user mode *) + let status = new MatitaEngine.status None baseuri in (match current with Some current -> NCicLibrary.time_travel status; @@ -341,6 +333,10 @@ object (self) ~callback:(fun () -> self#clean_dirty_lock)); ignore (GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackupFile ();true)); + ignore (buffer#connect#changed + (fun _ -> + let curpos = buffer#cursor_position in + HLog.debug ("cursor at " ^ (string_of_int curpos)))); ignore (buffer#connect#modified_changed (fun _ -> self#set_star buffer#modified)); (* clean_locked is set to true only "during" a PRIMARY paste @@ -673,26 +669,23 @@ object (self) in let time2 = Unix.gettimeofday () in HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s"); - let new_statuses, new_statements = - let statuses, texts = List.split entries in - statuses, texts - in - history <- new_statuses @ history; - statements <- new_statements @ statements; + let new_statuses, new_statements = entries in + history <- new_statuses :: history; + statements <- new_statements :: statements; let start = buffer#get_iter_at_mark (`MARK locked_mark) in - let new_text = String.concat "" (List.rev new_statements) in if statement <> None then - buffer#insert ~iter:start new_text + buffer#insert ~iter:start new_statements else begin let parsed_text = String.sub s 0 parsed_len in - if new_text <> parsed_text then begin + if new_statements <> parsed_text then begin let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in buffer#delete ~start ~stop; - buffer#insert ~iter:start new_text; + buffer#insert ~iter:start new_statements; end; end; - self#moveMark (Glib.Utf8.length new_text); - buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext + self#moveMark (Glib.Utf8.length new_statements); + buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) + newtext method private _retract offset status new_statements new_history = NCicLibrary.time_travel status; @@ -807,8 +800,78 @@ object (self) self#notify method loadFromFile f = - buffer#set_text (HExtlib.input_file f); + let script = HExtlib.input_file f in + let hs = MatitaScriptLexer.get_hot_spots script in + let hstext = + String.concat "\n" (List.map (fun (l1,l2,uri,desc) -> + let a,b = HExtlib.loc_of_floc l1 in + let c,d = HExtlib.loc_of_floc l2 in + let uri = match uri with None -> "()" | Some s -> s in + let desc = match desc with None -> "()" | Some s -> s in + Printf.sprintf "[%d,%d] [%d,%d] '%s' '%s'" a b c d uri desc) hs) + in + HLog.debug hstext; + buffer#set_text script; + + (* this is the default tag for the whole script (mainly used for + * setting the default behaviour when needed *) + let all_tag = buffer#create_tag [] in + buffer#apply_tag all_tag ~start:(buffer#get_iter `START) + ~stop:(buffer#get_iter `END); + ignore(all_tag#connect#event + ~callback:(fun ~origin event pos -> + match GdkEvent.get_type event with + | `MOTION_NOTIFY -> + Gdk.Window.set_cursor + (match source_view#get_window `TEXT with None -> assert false | Some x -> x) + (Gdk.Cursor.create `ARROW); + (* code for removing message from statusbar *) + false + | _ -> false)); + + let invisible_tag = buffer#create_tag [ `INVISIBLE true ] in + let apply_tag (l1,l2,uri,desc) = + let hyperlink_tag = + buffer#create_tag [ `FOREGROUND "blue" ; `UNDERLINE `SINGLE] in + (* hyperlink_tag#connect#after#changed ~callback:(fun _ -> HLog.debug "***"); *) + let a,b = HExtlib.loc_of_floc l1 in + let c,d = HExtlib.loc_of_floc l2 in + (* setting invisibility for and *) + buffer#apply_tag invisible_tag + ~start:(buffer#get_iter_at_char a) + ~stop:(buffer#get_iter_at_char b); + buffer#apply_tag invisible_tag + ~start:(buffer#get_iter_at_char c) + ~stop:(buffer#get_iter_at_char d); + (* setting hyperlink inside and *) + (* XXX: I'm not sure why I'm required to put those -1 and +1 + * otherwise I get too small a clickable area, especially for + * single characters hyperlinks. *) + buffer#apply_tag hyperlink_tag + ~start:(buffer#get_iter_at_char (b-1)) + ~stop:(buffer#get_iter_at_char (c+1)); + match uri with + | None -> () + | Some uri -> + ignore(hyperlink_tag#connect#event + ~callback:(fun ~origin event pos -> + match GdkEvent.get_type event with + `BUTTON_PRESS -> + let uri' = NReference.reference_of_string uri in + MatitaMathView.cicBrowser (Some (`NRef uri')); + true + | `MOTION_NOTIFY -> + Gdk.Window.set_cursor + (match source_view#get_window `TEXT with None -> assert false | Some x -> x) + (Gdk.Cursor.create `HAND1); + (* let ctxt = (MatitaMisc.get_gui ())#main#statusBar#new_context ~name:"href" in + let msg = ctxt#push uri in + (* href_statusbar_msg <- Some (ctxt, msg);*) *) + false + | _ -> false)) + in self#reset_buffer; + List.iter apply_tag hs; buffer#set_modified false method assignFileName file = @@ -960,29 +1023,7 @@ object (self) | _::[] -> true | _ -> false - method eos = - let rec is_there_only_comments status s = - if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let strm = - GrafiteParser.parsable_statement status - (Ulexing.from_utf8_string s)in - match GrafiteParser.parse_statement status strm with - | GrafiteAst.Comment (loc,_) -> - let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in - (* CSC: why +1 in the following lines ???? *) - let parsed_text_length = parsed_text_length + 1 in - let remain_len = String.length s - parsed_text_length in - let next = String.sub s parsed_text_length remain_len in - is_there_only_comments status next - | GrafiteAst.Executable _ -> false - in - try is_there_only_comments self#status self#getFuture - with - | NCicLibrary.IncludedFileNotCompiled _ - | HExtlib.Localized _ - | CicNotationParser.Parse_error _ -> false - | Margin | End_of_file -> true - | Invalid_argument "Array.make" -> false + method eos = MatitaEngine.eos self#status self#getFuture (* debug *) method dump () =