why.lang 6.9 KB
Newer Older
1
<?xml version="1.0" encoding="UTF-8"?>
2
<!--
3

4 5 6 7 8 9 10 11 12 13
Copyright (C) 2010-
  Francois Bobot
  Jean-Christophe Filliatre
  Johannes Kanig
  Andrei Paskevich
 
This software is free software; you can redistribute it and/or 
modify it under the terms of the GNU Library General Public 
License version 2.1, with the special exception on linking 
described in file LICENSE.
14

15 16 17 18 19 20 21 22 23
This software is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
-->
<!--
 This file was based on ocaml.lang by 
 Copyright (C) 2007 Eric Cooper <ecc@cmu.edu>
 Copyright (C) 2007 Eric Norige <thelema314@gmail.com>
-->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24
<language id="why" _name="Why3" version="2.0" _section="Sources">
25
  <metadata>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26
    <property name="mimetypes">text/x-why</property>
27
    <property name="globs">*.mlw;*.why</property>
28 29 30
    <property name="block-comment-start">(*</property>
    <property name="block-comment-end">*)</property>
  </metadata>
31

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
  <styles>
    <style id="comment" _name="Comment" map-to="def:comment"/>
    <style id="base-n-integer" _name="Base-N Integer" map-to="def:base-n-integer"/>
    <style id="floating-point" _name="Floating Point number" map-to="def:floating-point"/>
    <style id="decimal" _name="Decimal number" map-to="def:decimal"/>
    <style id="string" _name="String" map-to="def:string"/>
    <style id="keyword" _name="Keyword" map-to="def:keyword"/>
    <style id="meta-keyword" _name="Type, module or object keyword" map-to="def:keyword"/>
    <style id="fun-keyword" _name="Builtin-function keyword" map-to="def:keyword"/>
    <style id="type" _name="Data Type" map-to="def:type"/>
    <style id="label" _name="Labeled argument" map-to="def:type"/>
    <style id="poly-variant" _name="Polymorphic Variant" map-to="def:type"/>
    <style id="variant" _name="Variant Constructor" map-to="def:type"/>
    <style id="type-var" _name="Type Variable" map-to="def:type"/>
    <style id="module" _name="Module Path" map-to="def:type"/>
    <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
    <style id="boolean" _name="Boolean value" map-to="def:boolean"/>
    <style id="error" _name="Error" map-to="def:error"/>
  </styles>
51

52 53 54 55
  <definitions>
    <define-regex id="cap-ident">\b[A-Z][A-Za-z0-9_']*</define-regex>
    <define-regex id="low-ident">\b[a-z][A-Za-z0-9_']*</define-regex>
    <define-regex id="char-esc">\\((\\|"|'|n|t|b|r)|[0-9]{3}|x[0-9a-fA-F]{2})</define-regex>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
56
    <!-- " -->
57 58 59 60 61 62
    <context id="escape-seq" style-ref="escape">
      <match>\%{char-esc}</match>
    </context>
    <!-- here's the main context -->
    <context id="why">
      <include>
Andrei Paskevich's avatar
Andrei Paskevich committed
63
	<context id="symbol-star">
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64 65 66 67
	  <match>\(\*\)</match>
	</context>
	<context id="comment" style-ref="comment">
	  <start>\(\*</start>
68 69
	  <end>\*\)</end>
	  <include>
Andrei Paskevich's avatar
Andrei Paskevich committed
70
	    <context ref="symbol-star"/>
71 72 73 74 75
	    <context id="comment-in-comment" style-ref="comment">
	      <start>\(\*</start>
	      <end>\*\)</end>
	      <include>
		<context ref="string"/>
Andrei Paskevich's avatar
Andrei Paskevich committed
76
		<context ref="symbol-star"/>
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
		<context ref="comment-in-comment"/>
		<context ref="def:in-comment:*"/>
	      </include>
	    </context>
	    <context ref="string"/>
	    <context ref="def:in-comment:*"/>
	  </include>
	</context>
	<context id="decimal" style-ref="decimal">
	  <match>[-]?[0-9][0-9_]*[lLn]?</match>
	</context>
	<context id="hex-number" style-ref="base-n-integer">
	  <match>[-]?0[xX][0-9A-Fa-f][0-9A-Fa-f_]*[lL]?</match>
	</context>
	<context id="octal-number" style-ref="base-n-integer">
	  <match>[-]?0[oO][0-7][0-7_]*[lL]?</match>
	</context>
	<context id="binary-number" style-ref="base-n-integer">
	  <match>[-]?0[bB][01][01_]*[lL]?</match>
	</context>
	<context id="floating-point-number" style-ref="floating-point">
	  <match>[-]?[0-9][0-9_]*(\.[0-9_]*)?([Ee][+-]?[0-9][0-9_]*)?</match>
	</context>
	<context id="label" style-ref="label">
	  <match>[~?]\%{low-ident}</match>
	</context>
	<context id="poly-variant" style-ref="poly-variant">
	  <match>`\%{cap-ident}</match>
	</context>
	<context id="modpath" style-ref="module">
	  <!-- include final '.'?  At the moment, no.  -->
	  <match>\%{cap-ident}(\.\%{cap-ident})*(?=\.)</match>
	</context>
	<context id="variant" style-ref="variant">
	  <match>\%{cap-ident}</match>
	</context>
	<context id="string" style-ref="string">
	  <start>"</start>
	  <end>"</end>
	  <include>
	    <context ref="escape-seq"/>
	  </include>
	</context>
	<context id="character-constant" style-ref="string">
	  <match>('\%{char-esc}')|('[^\\']')</match>
	</context>
	<context id="type-var" style-ref="type-var">
	  <match>'\%{low-ident}</match>
	</context>
	<context id="arraylit">
	  <start>\[\|</start>
	  <end>\|\]</end>
	  <include>
	    <context ref="why"/>
	  </include>
	</context>
	<context id="badarray" style-ref="error" extend-parent="false">
	  <match>\|\]</match>
	</context>
	<context id="listlit">
	  <start>\[</start>
	  <end>(?&lt;!\|)\]</end>
	  <include>
	    <context ref="why"/>
	  </include>
	</context>
	<context id="badlist" style-ref="error" extend-parent="false">
	  <match>\]</match>
	</context>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
146
	<context id="keywords" style-ref="meta-keyword">
147 148 149 150 151
          <keyword>axiom</keyword>
          <keyword>clone</keyword>
          <keyword>end</keyword>
          <keyword>exception</keyword>
          <keyword>export</keyword>
152
          <keyword>constant</keyword>
153 154 155 156 157 158 159 160 161 162 163 164 165
          <keyword>function</keyword>
          <keyword>goal</keyword>
          <keyword>import</keyword>
          <keyword>inductive</keyword>
          <keyword>lemma</keyword>
          <keyword>module</keyword>
          <keyword>namespace</keyword>
          <keyword>predicate</keyword>
          <keyword>theory</keyword>
          <keyword>type</keyword>
          <keyword>use</keyword>
          <keyword>val</keyword>
          <keyword>with</keyword>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166 167
	</context>
	<context id="meta-words" style-ref="keyword">
168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
          <keyword>absurd</keyword>
          <keyword>assert</keyword>
          <keyword>begin</keyword>
          <keyword>do</keyword>
          <keyword>done</keyword>
          <keyword>downto</keyword>
          <keyword>else</keyword>
          <keyword>exists</keyword>
          <keyword>for</keyword>
          <keyword>forall</keyword>
          <keyword>if</keyword>
          <keyword>in</keyword>
          <keyword>invariant</keyword>
          <keyword>let</keyword>
          <keyword>match</keyword>
          <keyword>raise</keyword>
          <keyword>raises</keyword>
          <keyword>reads</keyword>
          <keyword>rec</keyword>
          <keyword>then</keyword>
          <keyword>to</keyword>
          <keyword>try</keyword>
          <keyword>variant</keyword>
          <keyword>while</keyword>
          <keyword>writes</keyword>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193
	  <keyword>-&gt;</keyword>
194 195 196
	</context>
	<context id="types" style-ref="type">
	  <!-- pervasives types -->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
197 198
	  <keyword>int</keyword>
 	  <keyword>real</keyword>
199
	</context>
200 201 202
	<context id="var">
	  <match>\%{low-ident}</match>
	</context>
203 204 205
      </include>
    </context>
  </definitions>
206
</language>