From 3d699c7323559951b3f8526308a6edee45203903 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 8 Oct 2024 15:17:22 +0200
Subject: [PATCH] [doc] terminology loader/importer
---
doc/userman/user-acsl.tex | 2 +-
src/plugins/wp/Why3Import.ml | 4 ++--
src/plugins/wp/doc/manual/wp_plugin.tex | 4 ++--
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 61cfff6e8f3..2656757db20 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -106,7 +106,7 @@ used, it is possible to have logic identifiers with an extended lexical format:
For instance, \verb+Foo::bar'jazz+ is a syntactically valid identifier.
\end{itemize}
-External module loaders are defined by plug-ins \textit{via} the extension API,
+External module importers are defined by plug-ins \textit{via} the extension API,
consult the plug-in manuals and the plug-in developer manual for more details.
%%% Local Variables:
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 47ffa89b754..fc5178e0d55 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -345,7 +345,7 @@ module Env = WpContext.StaticGenerator
add_builtins env ; env
end)
-let loader (ctxt: LT.module_builder) (_: C.location) (m: string list) =
+let importer (ctxt: LT.module_builder) (_: C.location) (m: string list) =
begin
L.debug ~dkey "Importing Why3 theory %s.@." (String.concat "::" m) ;
let thname = String.concat "." m in
@@ -360,7 +360,7 @@ let register () =
if not !registered then
begin
registered := true ;
- Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader ;
+ Acsl_extension.register_module_importer ~plugin:"wp" "why3" importer ;
end
let () = Cmdline.run_after_extended_stage register
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 591e53d4801..9ef08aa6f42 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1788,13 +1788,13 @@ by a link (`\user{link};'). The available tags are depicted on figure~\ref{wp-dr
\subsection{Importing Why3 Modules}
\label{importer}
-The \textsf{WP} plug-in provides an \textsf{ACSL} module loader that
+The \textsf{WP} plug-in provides an \textsf{ACSL} module importer that
can import \textsf{Why3} theories and modules into \textsf{ACSL}.
See \textsf{Frama-C} user manual, Section § 6.3 for details.
Here is an example of use:
\begin{lstlisting}
-//@ import why3: number::Gcd;
+//@ import \wp::why3: number::Gcd;
/*@
assigns \nothing;
--
GitLab