From 8f186be42e6cba96a6093eea0860f5a14ed80e71 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Jul 2005 14:17:37 +0000 Subject: [PATCH] Bug fixed: the _advance method must delete the parsed text iff it was parsed from the script itself (calling the getFuture method). --- helm/matita/matita.txt | 4 ++-- helm/matita/matitaScript.ml | 11 +++++++---- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 8c7e574f9..68b73f36c 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -47,8 +47,6 @@ TODO GUI GRAFICA - integrare il famoso logo mancante (anche nell'About dialog) - - quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo - dalla finestra principale!!! - highlight degli errori di parsing nello script (usando lo sfondo come per la parte lockata di testo, da ripulire quando si modifica il testo o si sposta il punto di esecuzione) @@ -80,6 +78,8 @@ TODO - non chiudere transitivamente i moo ?? DONE +- quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo + dalla finestra principale!!! -> CSC - sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza salvare. In verita' foo e' stato scritto lo stesso! -> CSC diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index ad1530d4e..4d092ca65 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -454,13 +454,16 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; statements <- List.rev new_statements @ statements; let start = buffer#get_iter_at_mark (`MARK locked_mark) in let new_text = String.concat "" new_statements in - if new_text <> String.sub s 0 parsed_len then + if statement <> None then + buffer#insert ~iter:start new_text + else + if new_text <> String.sub s 0 parsed_len then begin (* prerr_endline ("new:" ^ new_text); *) (* prerr_endline ("s:" ^ String.sub s 0 parsed_len); *) - let stop = start#copy#forward_chars parsed_len in - buffer#delete ~start ~stop; - buffer#insert ~iter:start new_text; + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop; + buffer#insert ~iter:start new_text; (* prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *) end; self#moveMark (String.length new_text) -- 2.39.2