Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
9bee04c0
Commit
9bee04c0
authored
Nov 28, 2011
by
Andrei Paskevich
Browse files
require %f in editor commands in config
parent
e1c5b8fe
Changes
4
Hide whitespace changes
Inline
Side-by-side
share/provers-detection-data.conf.in
View file @
9bee04c0
...
...
@@ -237,5 +237,5 @@ version_old = "8.1"
version_old = "8.0"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide -R %l/coq Why3"
editor = "coqide -R %l/coq Why3
%f
"
src/driver/call_provers.ml
View file @
9bee04c0
...
...
@@ -121,24 +121,24 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
let
arglist
=
Cmdline
.
cmdline_split
command
in
let
command
=
List
.
hd
arglist
in
let
on_timelimit
=
ref
false
in
let
on_filename
=
ref
false
in
let
cmd_regexp
=
Str
.
regexp
"%
\\
(.
\\
)"
in
let
replace
s
=
match
Str
.
matched_group
1
s
with
|
"%"
->
"%"
|
"f"
->
on_filename
:=
true
;
fin
|
"f"
->
fin
|
"t"
->
on_timelimit
:=
true
;
string_of_int
timelimit
|
"m"
->
string_of_int
memlimit
|
"b"
->
string_of_int
(
memlimit
*
1024
)
(* FIXME: libdir and datadir can be changed in the configuration file
Should we pass them as additional arguments? Or would it be better
to prepare the command line in a separate function? *)
|
"l"
->
Config
.
libdir
|
_
->
failwith
"unknown format specifier, use %%f, %%t, %%m or %%b"
|
"d"
->
Config
.
datadir
|
_
->
failwith
"unknown specifier, use %%f, %%t, %%m, %%l, or %%d"
in
let
subst
s
=
try
Str
.
global_substitute
cmd_regexp
replace
s
with
e
->
if
cleanup
then
Sys
.
remove
fin
;
raise
e
in
let
arglist
=
List
.
map
subst
arglist
in
let
argarray
=
Array
.
of_list
(
if
!
on_filename
then
arglist
else
arglist
@
[
fin
])
in
let
argarray
=
Array
.
of_list
(
List
.
map
subst
arglist
)
in
fun
()
->
let
fd_in
=
Unix
.
openfile
fin
[
Unix
.
O_RDONLY
]
0
in
...
...
src/driver/whyconf.ml
View file @
9bee04c0
...
...
@@ -30,10 +30,11 @@ open Rc
- 7 yices native (used for release 0.70)
- 8 for release 0.71
- 9 coq realizations
- 10 require %f in editor lines
If a configuration doesn't contain the actual magic number we don't use it.*)
let
magicnumber
=
9
let
magicnumber
=
10
exception
WrongMagicNumber
...
...
src/ide/gconfig.ml
View file @
9bee04c0
...
...
@@ -82,7 +82,9 @@ let default_ide =
ide_premise_color
=
"chartreuse"
;
ide_goal_color
=
"gold"
;
ide_error_color
=
"orange"
;
ide_default_editor
=
try
Sys
.
getenv
"EDITOR"
with
Not_found
->
"editor"
;
ide_default_editor
=
try
Sys
.
getenv
"EDITOR"
^
" %f"
with
Not_found
->
"editor %f"
;
}
let
load_ide
section
=
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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