Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
05014749
Commit
05014749
authored
Apr 08, 2010
by
Jean-Christophe Filliâtre
Browse files
sourceview -> sourceview2
parent
021a8131
Changes
4
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
05014749
...
...
@@ -273,11 +273,11 @@ ide-opt-yes: bin/whyide.opt
ide-opt-no
:
bin/whyide.opt
:
$(LIBCMXA) $(IDE_CMX)
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
$(OCAMLOPT)
$(OFLAGS)
-I
+threads
-o
$@
$(EXTCMXA)
threads.cmxa lablgtk.cmxa lablgtksourceview.cmxa gtkThread.cmx
$^
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
$(OCAMLOPT)
$(OFLAGS)
-I
+threads
-o
$@
$(EXTCMXA)
threads.cmxa lablgtk.cmxa lablgtksourceview
2
.cmxa gtkThread.cmx
$^
$(STRIP)
$@
bin/whyide.byte
:
$(GCMO)
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
$(OCAMLC)
$(BFLAGS)
-I
+threads
-o
$@
$(EXTCMA)
lablgtk.cma lablgtksourceview.cma threads.cma gtkThread.cmo
$^
$(
if
$(QUIET)
,@echo
'Linking $@'
&&
)
$(OCAMLC)
$(BFLAGS)
-I
+threads
-o
$@
$(EXTCMA)
lablgtk.cma lablgtksourceview
2
.cma threads.cma gtkThread.cmo
$^
include
.depend.ide
...
...
configure.in
View file @
05014749
...
...
@@ -259,9 +259,8 @@ dnl fi
# checking for lablgtk2
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,LABLGTK2=yes,LABLGTK2=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview.cma,LABLGTK2=yes,LABLGTK2=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview
2
.cma,LABLGTK2=yes,LABLGTK2=no)
# AC_CHECK_PROG(LABLGTK2,lablgtk2,yes,no) not always available (Win32)
# TODO: check gtksourceview
if test "$LABLGTK2" = yes ; then
INCLUDEGTK2="-I +lablgtk2"
fi
...
...
share/lang/why.lang
View file @
05014749
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE language SYSTEM "language.dtd">
<language
_name=
"Why"
version=
"1.0"
_section=
"Sources"
mimetypes=
"text/x-why"
>
<!--
<escape-char>
\
</escape-char>
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.
<block-comment
_name=
"Comment"
style=
"Comment"
end-at-line-end=
"FALSE"
>
<start-regex>
\(\*[^)*]
</start-regex>
<end-regex>
\*\)
</end-regex>
</block-comment>
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>
-->
<language
id=
"why"
_name=
"Objective Caml"
version=
"2.0"
_section=
"Sources"
>
<metadata>
<property
name=
"mimetypes"
>
text/x-ocaml
</property>
<property
name=
"globs"
>
*.ml;*.mli;*.mll;*.mly
</property>
<property
name=
"block-comment-start"
>
(*
</property>
<property
name=
"block-comment-end"
>
*)
</property>
</metadata>
<pattern-item
_name =
"Decimal"
style =
"Decimal"
>
<regex>
\b[-]?[0-9][0-9_]*[lL]?\b
</regex>
</pattern-item>
<styles>
<style
id=
"comment"
_name=
"Comment"
map-to=
"def:comment"
/>
<style
id=
"ocamldoc"
_name=
"Ocamldoc Comments"
map-to=
"def:note"
/>
<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>
<pattern-item
_name =
"Hex Number"
style =
"Base-N Integer"
>
<regex>
\b[-]?0[xX][0-9A-Fa-f][0-9A-Fa-f_]*[lL]?\b
</regex>
</pattern-item>
<pattern-item
_name =
"Octal Number"
style =
"Base-N Integer"
>
<regex>
\b[-]?0[oO][0-7][0-7_]*[lL]?\b
</regex>
</pattern-item>
<pattern-item
_name =
"Binary Number"
style =
"Base-N Integer"
>
<regex>
\b[-]?0[bB][01][01_]*[lL]?\b
</regex>
</pattern-item>
<pattern-item
_name =
"Floating Point Number"
style =
"Floating Point"
>
<regex>
\b[-]?[0-9][0-9_]*(\.[0-9_]*)?([Ee][+-]?[0-9][0-9_]*)?
</regex>
</pattern-item>
<string
_name =
"Character Constant"
style =
"String"
end-at-line-end =
"TRUE"
>
<start-regex>
'
</start-regex>
<end-regex>
'
</end-regex>
</string>
<string
_name =
"String"
style =
"String"
end-at-line-end =
"FALSE"
>
<start-regex>
"
</start-regex>
<end-regex>
"
</end-regex>
</string>
<pattern-item
_name =
"Modules"
style =
"Data Type"
case-sensitive=
"TRUE"
>
<regex>
\b[A-Z][A-Za-z0-9_']*
</regex>
</pattern-item>
<keyword-list
_name =
"Definition keyword"
style =
"Keyword"
case-sensitive=
"TRUE"
>
<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>
<context
id=
"escape-seq"
style-ref=
"escape"
>
<match>
\%{char-esc}
</match>
</context>
<!-- here's the main context -->
<context
id=
"why"
>
<include>
<context
id=
"ocamldoc"
style-ref=
"ocamldoc"
>
<start>
\(\*\*
</start>
<end>
\*\)
</end>
<include>
<context
id=
"comment-in-comment"
style-ref=
"comment"
>
<start>
\(\*
</start>
<end>
\*\)
</end>
<include>
<context
ref=
"string"
/>
<context
ref=
"comment-in-comment"
/>
<context
ref=
"def:in-comment:*"
/>
</include>
</context>
<context
ref=
"string"
/>
<context
ref=
"def:in-comment:*"
/>
</include>
</context>
<context
id=
"symbol-star"
style-ref=
"decimal"
>
<match>
\(\*\)
</match>
</context>
<context
id=
"comment"
style-ref=
"comment"
>
<start>
\(\*
</start>
<end>
\*\)
</end>
<include>
<context
ref=
"string"
/>
<context
ref=
"comment-in-comment"
/>
<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>
(?
<
!\|)\]
</end>
<include>
<context
ref=
"why"
/>
</include>
</context>
<context
id=
"badlist"
style-ref=
"error"
extend-parent=
"false"
>
<match>
\]
</match>
</context>
<context
id=
"boolean-constant"
style-ref=
"boolean"
>
<keyword>
true
</keyword>
<keyword>
false
</keyword>
</context>
<!-- Flow control & common keywords -->
<context
id=
"keywords"
style-ref=
"keyword"
>
<keyword>
theory
</keyword>
<keyword>
end
</keyword>
<keyword>
use
</keyword>
...
...
@@ -57,19 +169,22 @@
<keyword>
lemma
</keyword>
<keyword>
goal
</keyword>
<keyword>
type
</keyword>
</
keyword-lis
t>
<
keyword-list
_name =
"Expression key
word"
style
=
"Keyword"
case-sensitive=
"TRUE
"
>
</
contex
t>
<!-- types, objects and modules -->
<
context
id=
"meta-
word
s
"
style
-ref=
"meta-keyword
"
>
<keyword>
match
</keyword>
<keyword>
let
</keyword>
<keyword>
in
</keyword>
<keyword>
if
</keyword>
<keyword>
then
</keyword>
<keyword>
else
</keyword>
</
keyword-lis
t>
<keyword-list
_name =
"Types"
style =
"Data Type"
case-sensitive=
"TRUE"
>
</
contex
t>
<context
id=
"types"
style-ref=
"type"
>
<!-- pervasives types --
>
<keyword>
int
</keyword>
<keyword>
real
</keyword>
</keyword-list>
</context>
</include>
</context>
</definitions>
</language>
src/ide/ide_main.ml
View file @
05014749
...
...
@@ -46,17 +46,18 @@ let fname = match !file with
f
let
lang
=
let
file
=
let
load_path
=
List
.
fold_right
Filename
.
concat
[
Filename
.
dirname
Sys
.
argv
.
(
0
);
".."
;
"share"
;
"lang"
]
"why.
lang"
[
Filename
.
dirname
Sys
.
argv
.
(
0
);
".."
;
"share"
]
"
lang"
in
if
Sys
.
file_exists
file
then
let
languages_manager
=
GSourceView
.
source_languages_manager
()
in
GSourceView
.
source_language_from_file
~
languages_manager
file
else
begin
Format
.
eprintf
"could not find lang file (%S)@."
;
None
end
let
languages_manager
=
GSourceView2
.
source_language_manager
~
default
:
true
in
languages_manager
#
set_search_path
(
load_path
::
languages_manager
#
search_path
);
match
languages_manager
#
language
"why"
with
|
None
->
Format
.
eprintf
"pas trouv@;"
;
None
|
Some
_
as
l
->
l
let
text
=
let
ic
=
open_in
fname
in
...
...
@@ -174,21 +175,18 @@ let main () =
~
packing
:
hp
#
add
()
in
let
source_view
=
GSourceView
.
source_view
GSourceView
2
.
source_view
~
auto_indent
:
true
~
insert_spaces_instead_of_tabs
:
true
~
tab
s
_width
:
2
~
insert_spaces_instead_of_tabs
:
true
~
tab_width
:
2
~
show_line_numbers
:
true
~
margi
n
:
80
~
show_margin
:
true
~
smart_home_end
:
true
~
right_margin_positio
n
:
80
~
show_
right_
margin
:
true
(*
~smart_home_end:true
*)
~
packing
:
scrolled_win
#
add
~
height
:
500
~
width
:
650
()
in
source_view
#
misc
#
modify_font_by_name
font_name
;
begin
match
lang
with
|
Some
lang
->
source_view
#
source_buffer
#
set_language
lang
|
None
->
()
end
;
source_view
#
source_buffer
#
set_highlight
true
;
source_view
#
source_buffer
#
set_language
lang
;
source_view
#
set_highlight_current_line
true
;
source_view
#
source_buffer
#
set_text
text
;
w
#
add_accel_group
accel_group
;
...
...
@@ -200,6 +198,6 @@ let () =
(*
Local Variables:
compile-command: "unset LANG; make -C ../..
why-ide
-yes"
compile-command: "unset LANG; make -C ../..
ide-opt
-yes"
End:
*)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment