[devman] minor changes in documentation of the new Current_loc

doc/developer/advance.tex

@@ -1383,18 +1383,19 @@ specify a source location, either specifically or by using the current
 location of an \texttt{AST} visitor.
 \lstset{style=frama-c-style}
 \begin{itemize}
-\item[] \lstinline{~source:$s$} use the source location $s$ (see \texttt{Log.mli})
-\item[] \lstinline{~current:true} use the current source location
-  managed by \texttt{Current\_loc} (see \texttt{Current\_loc.mli}).
+\item[] \lstinline{~source:$s$} use the source position $s$ (see \texttt{Log.mli})
+\item[] \lstinline{~current:true} use the source location
+  managed by \texttt{Current\_loc} (see below).
 \end{itemize}
 
-\codeidxdef{Current\_loc}
-The current location is set manually, either by frama-c's kernel or by
-developpers in their plug-in. For instance \texttt{Cil} visitors update this
-location when visiting expressions, statements, globals, etc.
+\codeidxdef{Current\_loc}The \texttt{Current\_loc} module is used to
+manage the code location that is currently under focus.
+The current location must be set, either by \framac's kernel or by
+the plug-in themselves. In particular, \texttt{Cil} visitors update this
+location when visiting each node.
 
 \begin{example}
-  Different ways to set and use \texttt{Current\_loc}:
+The code samples below show how to use and set the current location.
   \scodeidx{Current\_loc}{let-bindings}
   \scodeidx{Current\_loc}{with\_loc\_opt}
   \scodeidx{Current\_loc}{with\_loc}
@@ -1409,33 +1410,27 @@ location when visiting expressions, statements, globals, etc.
      exceptions inside [f] will be caught and re-raised after resetting the
      location to its previous value. *)
   let apply_stmt f stmt =
-    Current_loc.with_loc (Cil_datatype.Stmt.loc s) f Stmt
+    Current_loc.with_loc (Cil_datatype.Stmt.loc s) f stmt
 
   (* [with_loc_opt opt_loc f x] behaves like [with_loc] if [loc_opt] is
      [Some loc], and does not update the current location if it is [None].*)
   let apply_code_annot f ca =
-    Current_loc.with_loc_opt (Cil_datatype.Code_annotation.loc s) f stmt
+    Current_loc.with_loc_opt (Cil_datatype.Code_annotation.loc ca) f ca
 
   (* Current_loc defines 2 let-binding operators which call [with_loc] and
      [with_loc_opt]. Here is a function that set the current location to the
      expr location, and reset it after the match. *)
   let do_expr e =
     let open Current_loc.Operators in
-    let$<>$ UpdatedCUrrentLoc = e.eloc in
+    let$<>$ UpdatedCurrentLoc = e.eloc in
     match e.enode with
     | ...
 
-  (* The same function after removing the let-binding syntax. Here [let$<>$] can
-     be replaced with [with_loc]. [UpdatedCUrrentLoc] is used as documentation
-     to know which operation is done by the operator, and to be sure we are
-     using the right one. It can be replaced by [_]. *)
-  let do_expr2 e =
+  (* When we only have a [loc option], we can use the $<?>$ operator *)
+  let do_code_annot f ca =
     let open Current_loc.Operators in
-    ( let$<>$ ) e.eloc (fun UpdatedCUrrentLoc ->
-      match e.enode with
-      | ...
-    ) UpdatedCUrrentLoc
-
+    let <?> UpdatedCurrentLoc = Cil_datatype.Code_annotation.loc ca in
+    f ca
   \end{ocamlcode}
   \end{example}
 

doc/developer/changes.tex

@@ -7,6 +7,7 @@ This chapter summarizes the major changes in this documentation between each
 
 \section*{Frama-C+dev}
 \begin{itemize}
+\item \textbf{Logging Services}: Document new \texttt{Current\_loc} module
 \item There is no more \texttt{Db} module:
   \begin{itemize}
   \item Whole document: \texttt{Db.Main.extend} is now \texttt{Boot.Main.extend}