From: Enrico Tassi Date: Tue, 31 May 2005 13:41:21 +0000 (+0000) Subject: fixed width fonts X-Git-Tag: PRE_INDEX_1~89 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e2beb1cd1269cc4dd94c184b85193f0fbc935324;p=helm.git fixed width fonts comments --- diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index f6cdff77d..4c53c5abc 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -225,6 +225,17 @@ class gui () = let buf = self#main#scriptTextView#buffer in buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n"; advance ()); + (* script monospace font stuff *) + let font = Pango.Font.from_string "Monospace 10" in + let monospace_tag = + self#main#scriptTextView#buffer#create_tag [`FONT_DESC font] + in + let _ = + self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ -> + let start, stop = self#main#scriptTextView#buffer#bounds in + self#main#scriptTextView#buffer#apply_tag monospace_tag start stop) + in + (* debug menu *) self#main#debugMenu#misc#hide (); (* status bar *) diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma index 6e5f59010..52c6d8476 100644 --- a/helm/matita/tests/comments.ma +++ b/helm/matita/tests/comments.ma @@ -1,3 +1,17 @@ +(****************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(****************************************************************************) + %% commento segato dal lexer (* commento che va nell'ast, ma non viene contato @@ -10,9 +24,13 @@ theorem a:0=0. %% commento segato dal lexer (* nota *) +(** + %% questo lo si vuole tenere anche dopo la hint -hint. +hint. +**) +apply cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1). (* commenti che non devono essere colorati perche' non c'e' nulla di eseguibile dopo di loro