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
fec2cd7b
Commit
fec2cd7b
authored
Mar 09, 2017
by
Jean-Christophe Filliâtre
Browse files
python plugin: parse function in Py_lexer
parent
33f8886f
Changes
2
Hide whitespace changes
Inline
Side-by-side
plugins/python/py_lexer.mll
View file @
fec2cd7b
...
...
@@ -149,6 +149,13 @@ and string = parse
List.iter (fun t -> Queue.add t tokens) l
end;
Queue.pop tokens
let parse file c =
let lb = Lexing.from_channel c in
Why3.Loc.set_file file lb;
stack := [0]; (* reinitialise indentation stack *)
Why3.Loc.with_location (Py_parser.file next_token) lb
}
...
...
plugins/python/py_main.ml
View file @
fec2cd7b
...
...
@@ -307,17 +307,14 @@ let translate ~loc inc (dl, s) =
inc
.
new_pdecl
loc
main
let
read_channel
env
path
file
c
=
let
lb
=
Lexing
.
from_channel
c
in
Loc
.
set_file
file
lb
;
let
loc
=
Loc
.
user_position
file
0
0
0
in
Py_lexer
.
stack
:=
[
0
];
(* reinitialise indentation stack *)
let
f
=
Loc
.
with_location
(
Py_parser
.
file
Py_lexer
.
next_token
)
lb
in
let
f
=
Py_lexer
.
parse
file
c
in
Debug
.
dprintf
debug
"%s parsed successfully.@."
file
;
let
file
=
Filename
.
basename
file
in
let
file
=
Filename
.
chop_extension
file
in
let
name
=
String
.
capitalize
file
in
Debug
.
dprintf
debug
"building module %s.@."
name
;
let
inc
=
Mlw_typing
.
open_file
env
path
in
let
loc
=
Why3
.
Loc
.
user_position
file
0
0
0
in
inc
.
open_module
(
mk_id
~
loc
name
);
let
use_import
(
f
,
m
)
=
let
q
=
Qdot
(
Qident
(
mk_id
~
loc
f
)
,
mk_id
~
loc
m
)
in
...
...
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