Merge pull request #1704 from triska/time_doc

DOC: correctly format the table using DocLog syntax
This commit is contained in:
Mark Thom
2023-01-25 22:51:05 +01:00
committed by GitHub

View File

@@ -28,32 +28,32 @@ current_time(T) :-
%% format_time(FormatString, TimeStamp)// %% format_time(FormatString, TimeStamp)//
% %
% The nonterminal format_time//2 describes a list of characters that % The nonterminal format_time//2 describes a list of characters that
% are formatted according to a format string. Usage: % are formatted according to a format string. Usage:
% %
% ``` % ```
% phrase(format_time(FormatString, TimeStamp), Cs) % phrase(format_time(FormatString, TimeStamp), Cs)
% ``` % ```
% %
% TimeStamp represents a moment in time in an opaque form, as for % TimeStamp represents a moment in time in an opaque form, as for
% example obtained by `current_time/1`. % example obtained by `current_time/1`.
% %
% FormatString is a list of characters that are interpreted literally, % FormatString is a list of characters that are interpreted literally,
% except for the following specifiers (and possibly more in the future): % except for the following specifiers (and possibly more in the future):
% %
% | %Y | year of the time stamp. Example: 2020. | % | `%Y` | year of the time stamp. Example: 2020. |
% | %m | month number (01-12), zero-padded to 2 digits | % | `%m` | month number (01-12), zero-padded to 2 digits |
% | %d | day number (01-31), zero-padded to 2 digits | % | `%d` | day number (01-31), zero-padded to 2 digits |
% | %H | hour number (00-24), zero-padded to 2 digits | % | `%H` | hour number (00-24), zero-padded to 2 digits |
% | %M | minute number (00-59), zero-padded to 2 digits | % | `%M` | minute number (00-59), zero-padded to 2 digits |
% | %S | second number (00-60), zero-padded to 2 digits | % | `%S` | second number (00-60), zero-padded to 2 digits |
% | %b | abbreviated month name, always 3 letters | % | `%b` | abbreviated month name, always 3 letters |
% | %a | abbreviated weekday name, always 3 letters | % | `%a` | abbreviated weekday name, always 3 letters |
% | %A | full weekday name | % | `%A` | full weekday name |
% | %j | day of the year (001-366), zero-padded to 3 digits | % | `%j` | day of the year (001-366), zero-padded to 3 digits |
% | %% | the literal % | % | `%%` | the literal `%` |
% %
% Example: % Example:
% %
% ``` % ```
% ?- current_time(T), phrase(format_time("%d.%m.%Y (%H:%M:%S)", T), Cs). % ?- current_time(T), phrase(format_time("%d.%m.%Y (%H:%M:%S)", T), Cs).