Skip to content

Commit

Permalink
Use lankit parser for syntax highlighting
Browse files Browse the repository at this point in the history 
Fixes eng/recordflux/RecordFlux#1290
  • Loading branch information
@senier
senier committed Sep 5, 2023
1 parent 7837f83 commit a79edc2
Show file tree
Hide file tree
Showing 9 changed files with 1,895 additions and 55 deletions.
5 changes: 5 additions & 0 deletions doc/language_reference/conf.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,12 @@
import sys
from pathlib import Path

from sphinx.highlighting import lexers

from rflx import __version__
from tools.rflxlexer import RFLXLexer

lexers["rflx"] = RFLXLexer(startinline=True)

# -- Path setup --------------------------------------------------------------

Expand Down
72 changes: 36 additions & 36 deletions doc/language_reference/language_reference.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ The bit size has to be specified explicitly.
**Example**

.. doc-check: rflx,basic_declaration,3
.. code:: ada
.. code:: rflx
type Type_Length is range 46 .. 2 ** 16 - 1 with Size => 16
Expand Down Expand Up @@ -100,12 +100,12 @@ A message field with such type is always considered valid, whether or not its va
**Example**

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Tag is (Msg_Error, Msg_Data) with Size => 1
.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Ether_Type is
(ET_IPv4 => 16#0800#,
Expand Down Expand Up @@ -218,7 +218,7 @@ All bytes which were received when parsing or were written when serializing are
**Example**

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Frame is
message
Expand All @@ -243,7 +243,7 @@ All bytes which were received when parsing or were written when serializing are
end message
.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Empty_Message is null message
Expand Down Expand Up @@ -273,7 +273,7 @@ To indicate that a refined field is empty (i.e. does not exit) under a certain c
**Example**

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
for Ethernet::Frame use (Payload => IPv4::Packet)
if Ether_Type = Ethernet::IPV4
Expand All @@ -300,7 +300,7 @@ Type refinements of a base message type are not inherited by the derived message
**Example**

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Specific_Extension is new Extension
Expand Down Expand Up @@ -329,7 +329,7 @@ Scalar types as well as message types can be used as element type.
**Example**

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Options is sequence of Option
Expand Down Expand Up @@ -361,7 +361,7 @@ The main part of a session definition are the state definitions.
**Example**

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
generic
X : Channel with Readable, Writable;
Expand Down Expand Up @@ -448,7 +448,7 @@ The return type and parameters of a function are represented by the first and su
**Example**

.. doc-check: rflx,session_parameter
.. code:: ada
.. code:: rflx
with function Decrypt
(Key_Update_Message : Key_Update_Message;
Expand Down Expand Up @@ -483,7 +483,7 @@ Channels can be readable or writable (non-exclusive).
**Example**

.. doc-check: rflx,session_parameter
.. code:: ada
.. code:: rflx
Data_Channel : Channel with Readable, Writable
Expand Down Expand Up @@ -544,7 +544,7 @@ A declared variable must have a type and can be optionally initialized using an
**Example**

.. doc-check: rflx,declaration
.. code:: ada
.. code:: rflx
Error_Sent : Boolean := False
Expand All @@ -562,7 +562,7 @@ Renaming Declaration
**Example**

.. doc-check: rflx,declaration
.. code:: ada
.. code:: rflx
Client_Hello_Message : TLS_Handshake::Client_Hello renames Client_Hello_Handshake_Message.Payload
Expand Down Expand Up @@ -615,7 +615,7 @@ If no condition could be fulfilled or no conditional transitions were defined, t
**Example**

.. doc-check: rflx,state,6
.. code:: ada
.. code:: rflx
state A
with Desc => "rfc1149.txt+51:4-52:9"
Expand Down Expand Up @@ -723,7 +723,7 @@ The transition target must be either a state name or `null`, which represents th
**Example**

.. doc-check: rflx,conditional_transition,9
.. code:: ada
.. code:: rflx
goto B
with Desc => "rfc1149.txt+45:4-47:8"
Expand Down Expand Up @@ -782,7 +782,7 @@ An assignment always creates a copy of the original object.
**Example**

.. doc-check: rflx,assignment_statement
.. code:: ada
.. code:: rflx
Error_Sent := True
Expand Down Expand Up @@ -828,7 +828,7 @@ All subsequent fields of the set message field are invalidated.
**Example**

.. doc-check: rflx,message_field_assignment_statement
.. code:: ada
.. code:: rflx
Packet.Length := 42
Expand Down Expand Up @@ -872,7 +872,7 @@ Appending an element to a sequence might lead to an exception transition.
**Example**

.. doc-check: rflx,attribute_statement
.. code:: ada
.. code:: rflx
Parameter_Request_List'Append (DHCP::Domain_Name_Option)
Expand Down Expand Up @@ -916,7 +916,7 @@ Extending a sequence might lead to an exception transition.
**Example**

.. doc-check: rflx,attribute_statement
.. code:: ada
.. code:: rflx
Parameter_Request_List'Extend (Parameters)
Expand Down Expand Up @@ -964,7 +964,7 @@ The existing state of a message or sequence is removed (and the corresponding bu
**Example**

.. doc-check: rflx,attribute_statement
.. code:: ada
.. code:: rflx
Message'Reset
Expand Down Expand Up @@ -1004,7 +1004,7 @@ The read attribute statement is used to retrieve a message from a channel.
**Example**

.. doc-check: rflx,attribute_statement
.. code:: ada
.. code:: rflx
Data_Channel'Read (Message)
Expand Down Expand Up @@ -1049,7 +1049,7 @@ This behavior will change in the future (cf. `#569 <https://github.com/AdaCore/
**Example**

.. doc-check: rflx,attribute_statement
.. code:: ada
.. code:: rflx
Data_Channel'Write (Message)
Expand Down Expand Up @@ -1101,15 +1101,15 @@ Insufficient memory during the message creation leads to an exception transition
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
TLS_Record::TLS_Record'(Tag => TLS_Record::Alert,
Legacy_Record_Version => TLS_Record::TLS_1_2,
Length => Alert_Message'Size / 8,
Fragment => Alert_Message'Opaque)
.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
Null_Message'(null message)
Expand Down Expand Up @@ -1155,12 +1155,12 @@ An aggregate is a collection of elements.
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
[0, 1, 2]
.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
[]
Expand Down Expand Up @@ -1286,7 +1286,7 @@ This behavior will change in the future (cf. `#569 <https://github.com/AdaCore/
**Example**

.. doc-check: rflx,extended_suffix
.. code:: ada
.. code:: rflx
Message'Valid
Expand Down Expand Up @@ -1331,7 +1331,7 @@ This behavior will change in the future (cf. `#569 <https://github.com/AdaCore/
**Example**

.. doc-check: rflx,extended_suffix
.. code:: ada
.. code:: rflx
Ethernet_Frame.Payload
Expand Down Expand Up @@ -1370,7 +1370,7 @@ This behavior will change in the future (cf. `#569 <https://github.com/AdaCore/
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
[for O in Offer.Options if O.Code = DHCP::DHCP_Message_Type_Option => O.DHCP_Message_Type]
Expand Down Expand Up @@ -1430,7 +1430,7 @@ Quantified expressions enable reasoning about properties of sequences.
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
for all E in Server_Hello_Message.Extensions => E.Tag /= TLS_Handshake::ET_Supported_Versions
Expand Down Expand Up @@ -1471,7 +1471,7 @@ All functions which are declared in the session parameters can be called.
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
Decrypt (Key_Update_Message, Sequence_Number, TLS_Record_Message.Encrypted_Record)
Expand Down Expand Up @@ -1520,7 +1520,7 @@ This behavior will change in the future (cf. `#569 <https://github.com/AdaCore/
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
Key_Update_Message (Handshake_Control_Message.Data)
Expand Down Expand Up @@ -1551,7 +1551,7 @@ Two distinct `discrete choices <#grammar-token-discrete_choice>`_ of a `case exp
**Example**

.. doc-check: rflx,extended_primary
.. code:: ada
.. code:: rflx
(case Value is
when T::V1 | T::V2 => 2,
Expand All @@ -1578,7 +1578,7 @@ By convention one protocol is specified in one package.
**Example**

.. doc-check: rflx
.. code:: ada
.. code:: rflx
package Ethernet is
Expand Down Expand Up @@ -1660,7 +1660,7 @@ For each package referenced in a file, a corresponding with clause has to be add
**Example**

.. doc-check: rflx,context_clause
.. code:: ada
.. code:: rflx
with Ethernet;
with IPv4;
Expand All @@ -1683,7 +1683,7 @@ The file name must match the package name in lower case characters.
File: ``in_ethernet.rflx``.

.. doc-check: rflx,specification,0
.. code:: ada
.. code:: rflx
with Ethernet;
with IPv4;
Expand Down
15 changes: 7 additions & 8 deletions doc/user_guide/20-overview.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ There is exactly one package per file; the file name has to be the same as the p
We will use the name “Pub Sub” for our example protocol and create a file named `pub_sub.rflx` for the specification:

.. doc-check: rflx
.. code:: ada
.. code:: rflx
package Pub_Sub is
-- Type specifications (basic types, messages) go here
Expand All @@ -215,7 +215,7 @@ To limit the size and allowed values of a numeric field in a message, we need to
For the `Identifier` field we define a type that can represent values from 1 to 4000, inclusive, and whose instances occupy 12 bits:

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Identifier is range 1 .. 16#F_A0# with Size => 12
Expand All @@ -241,7 +241,7 @@ While we could even express the fact that the type field must not be zero by cho
An enumeration type is much better suited to represent discrete choices as in the Command field:

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Command is
(
Expand Down Expand Up @@ -283,13 +283,13 @@ Just like scalars, messages are also types.
The specification for our pub-sub message is as follows:

.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Length is range 0 .. 2 ** 8 - 1 with Size => 8
.. doc-check: rflx,basic_declaration
.. code:: ada
.. code:: rflx
type Message is
message
Expand Down Expand Up @@ -331,7 +331,7 @@ Among other things, the RecordFlux Verifier ensures that `then`-clauses are mutu
If we changed the above example to contain two `then`-clauses for Command which are not mutually exclusive, our specification would get rejected:

.. doc-check: ignore
.. code:: ada
.. code:: rflx
Command : Command
then Length
Expand Down Expand Up @@ -367,8 +367,7 @@ The RecordFlux Modeller can also be used to create and check specifications.
A simple project file named `pub_sub.gpr` located in the root directory of our example project configures directories for hand-written code (`src`), generated code (`generated`) and specifications (`specs`).
It also enables support for the RecordFlux specification language and sets the output directory for generated code:

.. doc-check: ignore
.. code:: ada
.. code::
project Pub_Sub is
Expand Down
Loading

0 comments on commit a79edc2

Please sign in to comment.