From d541d1b9cc3cffedf0d1903a39cd4683e1e6ef97 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 5 Oct 2010 15:21:46 +0000 Subject: [PATCH] -textual widget no longer editable --- matita/matita/matitaMathView.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 3f538ac45..f11354904 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -205,7 +205,8 @@ object (self) initializer self#set_font_size !current_font_size; self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang); - self#source_buffer#set_highlight_syntax true + self#source_buffer#set_highlight_syntax true; + self#set_editable false (* MATITA1.0 inherit GMathViewAux.multi_selection_math_view obj -- 2.39.2