Mentions légales du service

Skip to content

Improve ctrll

DAILLER Sylvain requested to merge improve_ctrll into master

This is a suggestion by @paskevyc to use the same process as why3doc for detecting an ident. why3doc uses a table from location to ident to know at which location each ident is defined: this is saved during parsing/typing using the flag Glob.flag.

This MR generalizes the use of Glob so that it is used with why3ide too: the flag is now set in why3ide.

A notable change in Glob is the use of nested hashtbls: one hashtbl per file. This allows us to erase an hashtbl contents when reading a file again (it avoids inconsistent locations see first commit).

Edited by DAILLER Sylvain

Merge request reports