From: Stefano Zacchiroli Date: Mon, 17 Jul 2006 09:49:44 +0000 (+0000) Subject: real life implementation of the highlighting, added css X-Git-Tag: make_still_working~7062 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=911b2823c0e495fdebf487ad55f7c06eaabfd95f;p=helm.git real life implementation of the highlighting, added css --- diff --git a/helm/www/matita/grafite-format.css b/helm/www/matita/grafite-format.css new file mode 100644 index 000000000..a02229d7e --- /dev/null +++ b/helm/www/matita/grafite-format.css @@ -0,0 +1,41 @@ + +.grafite_TheoremKinds { + color: #7779bb; + font-weight: bold; +} + +.grafite_Commands { + color: #200080; + font-weight: bold; +} + +.grafite_Tactics { + color: #930000; + font-style: italic; +} + +.grafite_Macros { + color: #004a43; +} + +.grafite_Sorts { + color: #7779bb; +} + +.grafite_Operators { + color: #44aadd; +} + +.grafite_String { + color: #1060b6; +} + +.grafite_Comment { + color: #595979; +} + +.grafite_Symbols { + color: #406080; + font-weight: bold; +} + diff --git a/helm/www/matita/grafite.hrc b/helm/www/matita/grafite.hrc index 4b88fa91d..7ebf82f63 100644 --- a/helm/www/matita/grafite.hrc +++ b/helm/www/matita/grafite.hrc @@ -1,188 +1,179 @@ - - - - \ - - - \(\*\*[^\)] - [^\(]\*\*\) - - - - \(\* - \*\) - - - - theorem - definition - lemma - fact - remark - variant - axiom - - - - alias - and - as - coercion - coinductive - corec - default - for - include - include' - inductive - in - interpretation - let - match - names - notation - on - qed - rec - record - return - to - using - with - - - - \[ - - - \| - - - \] - - - \{ - - - \} - - - @ - - - \$ - - - - Set - Prop - Type - - - - absurd - apply - assumption - auto - paramodulation - clear - clearbody - change - constructor - contradiction - cut - decompose - discriminate - elim - elimType - exact - exists - fail - fold - fourier - fwd - generalize - goal - id - injection - intro - intros - inversion - lapply - linear - left - letin - normalize - reduce - reflexivity - replace - rewrite - ring - right - symmetry - simplify - split - to - transitivity - unfold - whd - - - - try - solve - do - repeat - first - focus - unfocus - - - - - check - hint - set - - - - elim - hint - instance - locate - match - - - - def - forall - lambda - to - exists - Rightarrow - Assign - land - lor - lnot - liff - subst - vdash - iforall - iexists - - - - " - " - - - + + + + + + + + Grafite: Matita scripts language + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/www/matita/helm-proto.hrc b/helm/www/matita/helm-proto.hrc index f67842452..90b623542 100644 --- a/helm/www/matita/helm-proto.hrc +++ b/helm/www/matita/helm-proto.hrc @@ -17,6 +17,8 @@ /\.ma$/i - + + + diff --git a/helm/www/matita/navy.css b/helm/www/matita/navy.css new file mode 100644 index 000000000..335b37276 --- /dev/null +++ b/helm/www/matita/navy.css @@ -0,0 +1,247 @@ +/* Generated with hrd2css.pl from ./Colorer-take5.beta4/hrd/rgb/navy.hrd */ + +.def_HorzCross { + color: #000000; + background-color: #e8e7f8; +} + +.def_VertCross { + color: #000000; + background-color: #e1e0f2; +} + +.def_Number { + color: #008c00; +} + +.def_NumberDec { + color: #008c00; +} + +.def_NumberHex { + color: #008000; +} + +.def_NumberBin { + color: #005b00; +} + +.def_NumberOct { + color: #008c00; +} + +.def_NumberFloat { + color: #008000; +} + +.def_NumberSuffix { + color: #006600; +} + +.def_String { + color: #1060b6; +} + +.def_StringContent { + color: #0f69ff; +} + +.def_StringEdge { + color: #800000; +} + +.def_CharacterContent { + color: #0000cc; +} + +.def_Comment { + color: #595979; +} + +.def_CommentContent { + color: #7F9FBF; + font-weight: bold; +} + +.def_CommentEdge { + color: #606090; +} + +.def_CommentDoc { + color: #3F7F8F; +} + +.def_CommentDocEdge { + color: #c0bd92; +} + +.def_Symbol { + color: #308080; +} + +.def_SymbolStrong { + color: #406080; +} + +.def_Prefix { + color: #0066ee; +} + +.def_Operator { + color: #44aadd; +} + +.def_Keyword { + color: #200080; + font-weight: bold; +} + +.def_KeywordStrong { + color: #7779bb; + font-weight: bold; +} + +.def_FunctionKeyword { + color: #400000; +} + +.def_DeprecatedKeyword { + color: #008484; +} + +.def_InterfaceKeyword { + color: #008484; +} + +.def_ClassKeyword { + color: #6679aa; + font-weight: bold; +} + +.def_StructKeyword { + color: #003060; +} + +.def_TypeKeyword { + color: #7779bb; +} + +.def_Register { + color: #000080; +} + +.def_Constant { + color: #7d0045; +} + +.def_Var { + color: #007d45; +} + +.def_VarStrong { + color: #007997; +} + +.def_Identifier { + color: #005fd2; +} + +.def_BooleanConstant { + color: #0f4d75; +} + +.def_Directive { + color: #004a43; +} + +.def_Parameter { + color: #074726; +} + +.def_ParameterUnknown { + color: #474796; +} + +.def_Tag { + color: #333385; +} + +.def_OpenTag { + color: #0057a6; +} + +.def_CloseTag { + color: #0057a6; +} + +.def_Label { + color: #e34adc; +} + +.def_LabelStrong { + color: #000000; + background-color: #a8a800; +} + +.def_Insertion { + color: #000000; + background-color: #cceeee; +} + +.def_Error { + color: #ffffff; + background-color: #dd9999; + font-weight: bold; + font-style: italic; +} + +.def_ErrorText { + color: #ee00ee; +} + +.def_TODO { + color: #ffffff; + background-color: #808000; +} + +.def_Debug { + color: #80abfd; + background-color: #007084; +} + +.def_Path { + color: #40015a; +} + +.def_URL { + color: #5555DD; +} + +.def_EMail { + color: #7144c4; +} + +.def_Date { + color: #009797; +} + +.def_Time { + color: #8745a0; +} + +.def_PairStart { + color: #d0d0ff; +} + +.def_PairEnd { + color: #d0d0ff; +} + +.def_PairStrongStart { + color: #880088; +} + +.def_PairStrongEnd { + color: #880088; +} +