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
;;
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
(* 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
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)
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
| `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
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
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;
~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
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;
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 <A...> and </A> *)
+ 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 <A...> and </A> *)
+ (* 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 =
| _::[] -> 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 () =
projects / helm.git / blobdiff