Merge remote-tracking branch 'niklas/typeid' into typeid

README.rst

@@ -488,11 +488,11 @@ Other proof assistants
 Lean 4
 ------
 
-Alectryon has support for the Lean 4. LeanInk (`LeanInk <https://github.com/insightmind/LeanInk>`_) is required to use Alectryon with Lean 4 files.
+Alectryon has support for Lean 4. LeanInk (`LeanInk <https://github.com/leanprover/LeanInk>`_) is required to use Alectryon with Lean 4 files.
 HTML and LaTeX output is supported from plain ``.lean`` source files and from ``.rst`` files.
-The reStructuredText directive for Lean 4 is ``.. lean4::``, for Markdown/MyST files it is ``{lean4}``. The literate delimiter is ``/-|``.
+The reStructuredText directive for Lean 4 is ``.. lean4::``, for Markdown/MyST files it is ``{lean4}``. The literate delimiter is ``/-!``:
 
-- Lean 4 code in reStructuredText files, like this:
+- Include Lean 4 code in reStructuredText files like this:
 
   .. code-block:: rst
 
@@ -502,15 +502,15 @@ The reStructuredText directive for Lean 4 is ``.. lean4::``, for Markdown/MyST f
 
         … some Lean 4 code
 
-- reStructuredText prose in Lean 4 files, like this:
+- Include reStructuredText prose in Lean 4 files like this:
 
   .. code-block:: lean
 
      … some Lean 4 code
 
-     /-|
+     /-!
      Some reST prose.
-     |-/
+     -/
 
 See `<recipes/plain-lean4.lean>`__, `<recipes/lean4-tactics.rst>`__, `<recipes/lean4-tactics-myst.md>`__ and `<recipes/literate-lean4.lean>`__  for examples.
 
@@ -521,9 +521,9 @@ Lean 3
 
 Alectryon has preliminary support for Lean 3.
 
-Recording Lean's output and generating HTML or LaTeX is supported, from plain ``.lean`` files and from ``.rst`` files using the ``.. lean3::`` directive (as well as Markdown/MyST files using the ``{lean3}`` directive).  Language-agnostic features like caching work.  The literate delimiter is ``/-|``; in other words, you may write:
+Recording Lean's output and generating HTML or LaTeX is supported, from plain ``.lean`` files and from ``.rst`` files using the ``.. lean3::`` directive (as well as Markdown/MyST files using the ``{lean3}`` directive).  Language-agnostic features like caching work.  The literate delimiter is ``/-!``; in other words, you may write:
 
-- Lean 3 code in reStructuredText files, like this:
+- Include Lean 3 code in reStructuredText files like this:
 
   .. code-block:: rst
 
@@ -533,15 +533,15 @@ Recording Lean's output and generating HTML or LaTeX is supported, from plain ``
 
         … some Lean 3 code
 
-- reStructuredText prose in Lean3 files, like this:
+- Include reStructuredText prose in Lean 3 files like this:
 
   .. code-block:: lean
 
      … some Lean 3 code
 
-     /-|
+     /-!
      Some reST prose.
-     |-/
+     -/
 
 See `<recipes/plain-lean3.lean>`__ and `<recipes/lean3-tutorial.rst>`__ for examples.
 

alectryon/cli.py

@@ -430,7 +430,7 @@ def write_file(ext, strip):
 EXTENSIONS_BY_LANGUAGE = {
     "coq": (".v",),
     "lean4": (".lean",),
-    "lean3": (".lean", ".lean3"),
+    "lean3": (".lean3",),
 }
 
 assert EXTENSIONS_BY_LANGUAGE.keys() == core.ALL_LANGUAGES

alectryon/literate.py

@@ -805,19 +805,19 @@ def rst2code(lang: LangDef, rst):
     ...
     ...      1 + 1
     ... '''))
-    /-|
+    /-!
     Example:
-    |-/
+    -/
     <BLANKLINE>
     def x :=
     <BLANKLINE>
-    /-|
+    /-!
     Second example:
     <BLANKLINE>
     .. lean3::
        :name:
           snd
-    |-/
+    -/
     <BLANKLINE>
       1 + 1
     <BLANKLINE>
@@ -849,8 +849,8 @@ def rst2coq(rst):
 LEAN3 = LangDef(
     "lean3",
     LeanParser,
-    lit_open=r"/-|", lit_close=r"|-/",
-    lit_open_re=r"[/][-][|][ \t]*", lit_close_re=r"[ \t]*[|]?[-][/]\Z",
+    lit_open=r"/-!", lit_close=r"-/",
+    lit_open_re=r"[/][-][!][ \t]*", lit_close_re=r"[ \t]*[-][/]\Z",
     quote_pairs=[("/-", r"/\ -"), ("-/", r"-\ /")]
 )
 
@@ -865,8 +865,8 @@ def rst2lean3(rst):
 LEAN4 = LangDef(
     "lean4",
     LeanParser, # We can use the same parser as Lean 3, because the syntax for comments has not changed between the versions.
-    lit_open=r"/-|", lit_close=r"-/",
-    lit_open_re=r"[/][-][|][ \t]*", lit_close_re=r"[ \t]*?[-][/]\Z",
+    lit_open=r"/-!", lit_close=r"-/",
+    lit_open_re=r"[/][-][!][ \t]*", lit_close_re=r"[ \t]*[-][/]\Z",
     quote_pairs=[("/-", r"/\ -"), ("-/", r"-\ /")]
 )