all: Remove Coq prefix in Python and change coq- to alectryon- in CSS

CHANGES.rst

@@ -5,5 +5,6 @@
 Version 1.1
 ===========
 
+- Rename CSS classes from ``.coq-…`` to ``.alectryon-…``.
 - Rename CSS class ``alectryon-header`` to ``alectryon-banner``.
 - Remove the undocumented ``alectryon-header`` directive.

alectryon/core.py

@@ -40,17 +40,17 @@ class GeneratorInfo(namedtuple("GeneratorInfo", "name version")):
     def fmt(self, include_version_info=True):
         return "{} v{}".format(self.name, self.version) if include_version_info else self.name
 
-CoqHypothesis = namedtuple("CoqHypothesis", "names body type")
-CoqGoal = namedtuple("CoqGoal", "name conclusion hypotheses")
-CoqMessage = namedtuple("CoqMessage", "contents")
-CoqSentence = namedtuple("CoqSentence", "contents messages goals")
-CoqText = namedtuple("CoqText", "contents")
-
-CoqGoals = namedtuple("CoqGoals", "goals")
-CoqMessages = namedtuple("CoqMessages", "messages")
+Hypothesis = namedtuple("Hypothesis", "names body type")
+Goal = namedtuple("Goal", "name conclusion hypotheses")
+Message = namedtuple("Message", "contents")
+Sentence = namedtuple("Sentence", "contents messages goals")
+Text = namedtuple("Text", "contents")
+
+Goals = namedtuple("Goals", "goals")
+Messages = namedtuple("Messages", "messages")
 RichSentence = namedtuple("RichSentence", "contents outputs annots prefixes suffixes")
 
-CoqPrettyPrinted = namedtuple("CoqPrettyPrinted", "sid pp")
+PrettyPrinted = namedtuple("PrettyPrinted", "sid pp")
 
 def sexp_hd(sexp):
     if isinstance(sexp, list):
@@ -71,6 +71,9 @@ class SerAPI():
     SERTOP_BIN = "sertop"
     DEFAULT_ARGS = ("--printer=sertop", "--implicit")
 
+    # FIXME Pass -topfile (some file in the stdlib fail to compile without it)
+    # FIXME Pass --debug when invoked with --traceback
+
     MIN_PP_MARGIN = 20
     DEFAULT_PP_ARGS = {'pp_depth': 30, 'pp_margin': 55}
 
@@ -142,14 +145,14 @@ def _deserialize_hyp(sexp):
         assert len(body) <= 1
         body = body[0] if body else None
         ids = [sx.tostr(p[1]) for p in meta if p[0] == b'Id']
-        yield CoqHypothesis(ids, body, htype)
+        yield Hypothesis(ids, body, htype)
 
     @staticmethod
     def _deserialize_goal(sexp):
         name = dict(sexp[b'info'])[b'name']
         hyps = [h for hs in reversed(sexp[b'hyp'])
                 for h in SerAPI._deserialize_hyp(hs)]
-        return CoqGoal(dict(name).get(b'Id'), sexp[b'ty'], hyps)
+        return Goal(dict(name).get(b'Id'), sexp[b'ty'], hyps)
 
     @staticmethod
     def _deserialize_answer(sexp):
@@ -245,7 +248,7 @@ def _collect_messages(self, types, chunk, sid):
 
     def _pprint(self, sexp, sid, kind, pp_depth, pp_margin):
         if sexp is None:
-            return CoqPrettyPrinted(sid, None)
+            return PrettyPrinted(sid, None)
         if kind is not None:
             sexp = [kind, sexp]
         meta = [[b'sid', sid],
@@ -257,7 +260,7 @@ def _pprint(self, sexp, sid, kind, pp_depth, pp_margin):
         strings = list(self._collect_messages(ApiString, None, sid))
         if strings:
             assert len(strings) == 1
-            return CoqPrettyPrinted(sid, strings[0].string)
+            return PrettyPrinted(sid, strings[0].string)
         raise ValueError("No string found in Print answer")
 
     def _pprint_message(self, msg):
@@ -290,26 +293,26 @@ def _pprint_hyp(self, hyp, sid):
         w = max(self.pp_args['pp_margin'] - name_w, SerAPI.MIN_PP_MARGIN)
         body = self._pprint(hyp.body, sid, b'CoqExpr', d, w - 2).pp
         htype = self._pprint(hyp.type, sid, b'CoqExpr', d, w - 3).pp
-        return CoqHypothesis(hyp.names, body, htype)
+        return Hypothesis(hyp.names, body, htype)
 
     def _pprint_goal(self, goal, sid):
         ccl = self._pprint(goal.conclusion, sid, b'CoqExpr', **self.pp_args).pp
         hyps = [self._pprint_hyp(h, sid) for h in goal.hypotheses]
-        return CoqGoal(sx.tostr(goal.name) if goal.name else None, ccl, hyps)
+        return Goal(sx.tostr(goal.name) if goal.name else None, ccl, hyps)
 
     def _goals(self, sid, chunk):
         # LATER Goals instead and CoqGoal and CoqConstr?
         # LATER We'd like to retrieve the formatted version directly
         self._send([b'Query', [[b'sid', sid]], b'EGoals'])
-        goals = list(self._collect_messages(CoqGoal, chunk, sid))
+        goals = list(self._collect_messages(Goal, chunk, sid))
         yield from (self._pprint_goal(g, sid) for g in goals)
 
     def run(self, chunk):
         """Send a `chunk` to sertop.
 
         A chunk is a string containing Coq sentences or comments.  The sentences
-        are split, sent to Coq, and returned as a list of ``CoqText`` instances
-        (for whitespace and comments) and ``CoqSentence`` instances (for code).
+        are split, sent to Coq, and returned as a list of ``Text`` instances
+        (for whitespace and comments) and ``Sentence`` instances (for code).
         """
         if isinstance(chunk, str):
             chunk = chunk.encode("utf-8")
@@ -319,11 +322,11 @@ def run(self, chunk):
         for span_id, contents in spans:
             contents = str(contents, encoding='utf-8')
             if span_id is None:
-                fragments.append(CoqText(contents))
+                fragments.append(Text(contents))
             else:
                 messages.extend(self._exec(span_id, chunk))
                 goals = list(self._goals(span_id, chunk))
-                fragment = CoqSentence(contents, messages=[], goals=goals)
+                fragment = Sentence(contents, messages=[], goals=goals)
                 fragments.append(fragment)
                 fragments_by_id[span_id] = fragment
         # Messages for span n + δ can arrive during processing of span n or
@@ -335,19 +338,19 @@ def run(self, chunk):
                 MSG = "!! Orphaned message for sid {}:{}\n"
                 stderr.write(MSG.format(message.sid, pp))
             else:
-                fragment.messages.append(CoqMessage(message.pp))
+                fragment.messages.append(Message(message.pp))
         return fragments
 
 def annotate(chunks, sertop_args=()):
     """Annotate multiple `chunks` of Coq code.
 
     All fragments are executed in the same Coq instance, started with arguments
     `sertop_args`.  The return value is a list with as many elements as in
-    `chunks`, but each element is a list of fragments: either ``CoqText``
-    instances (whitespace and comments) and ``CoqSentence`` instances (code).
+    `chunks`, but each element is a list of fragments: either ``Text``
+    instances (whitespace and comments) and ``Sentence`` instances (code).
 
     >>> annotate(["Check 1."], ("-Q", "..,logical_name"))
-    [[CoqSentence(contents='Check 1.', messages=[CoqMessage(contents='1\n     : nat')], goals=[])]]
+    [[Sentence(contents='Check 1.', messages=[Message(contents='1\n     : nat')], goals=[])]]
     """
     with SerAPI(args=sertop_args) as api:
         return [api.run(chunk) for chunk in chunks]

alectryon/html.py

@@ -24,7 +24,7 @@
 
 from dominate import tags
 
-from .core import CoqText, RichSentence, CoqGoals, CoqMessages
+from .core import Text, RichSentence, Goals, Messages
 from . import transforms, GENERATOR
 
 _SELF_PATH = path.dirname(path.realpath(__file__))
@@ -111,7 +111,7 @@ def gen_hyps(self, hyps):
 
     def gen_goal(self, goal, toggle=None):
         """Serialize a goal to HTML."""
-        with tags.blockquote(cls="coq-goal"):
+        with tags.blockquote(cls="alectryon-goal"):
             if goal.hypotheses:
                 # Chrome doesn't support the ‘gap’ property in flex containers,
                 # so properly spacing hypotheses requires giving them margins
@@ -120,7 +120,7 @@ def gen_goal(self, goal, toggle=None):
                 # there are none.
                 self.gen_hyps(goal.hypotheses)
             toggle = goal.hypotheses and toggle
-            cls = "goal-separator" + (" coq-extra-goal-label" if toggle else "")
+            cls = "goal-separator" + (" alectryon-extra-goal-label" if toggle else "")
             with self.gen_label(toggle, cls):
                 tags.hr()
                 if goal.name:
@@ -138,45 +138,45 @@ def gen_checkbox(self, checked, cls):
     def gen_goals(self, first, more):
         self.gen_goal(first)
         if more:
-            with tags.div(cls='coq-extra-goals'):
+            with tags.div(cls='alectryon-extra-goals'):
                 for goal in more:
-                    nm = self.gen_checkbox(False, "coq-extra-goal-toggle")
+                    nm = self.gen_checkbox(False, "alectryon-extra-goal-toggle")
                     self.gen_goal(goal, toggle=nm)
 
     def gen_input_toggle(self, fr):
         if not fr.outputs:
             return None
-        return self.gen_checkbox(fr.annots.unfold, "coq-toggle")
+        return self.gen_checkbox(fr.annots.unfold, "alectryon-toggle")
 
     def gen_input(self, fr, toggle):
-        cls = "coq-input" + (" alectryon-failed" if fr.annots.fails else "")
+        cls = "alectryon-input" + (" alectryon-failed" if fr.annots.fails else "")
         self.gen_label(toggle, cls, self.highlight(fr.contents))
 
     def gen_output(self, fr):
         # Using <small> improves rendering in RSS feeds
-        wrapper = tags.div(cls="coq-output-sticky-wrapper")
-        with tags.small(cls="coq-output").add(wrapper):
+        wrapper = tags.div(cls="alectryon-output-sticky-wrapper")
+        with tags.small(cls="alectryon-output").add(wrapper):
             for output in fr.outputs:
-                if isinstance(output, CoqMessages):
+                if isinstance(output, Messages):
                     assert output.messages, "transforms.commit_io_annotations"
-                    with tags.div(cls="coq-messages"):
+                    with tags.div(cls="alectryon-messages"):
                         for message in output.messages:
                             tags.blockquote(self.highlight(message.contents),
-                                            cls="coq-message")
-                if isinstance(output, CoqGoals):
+                                            cls="alectryon-message")
+                if isinstance(output, Goals):
                     assert output.goals, "transforms.commit_io_annotations"
-                    with tags.div(cls="coq-goals"):
+                    with tags.div(cls="alectryon-goals"):
                         self.gen_goals(output.goals[0], output.goals[1:])
 
     @staticmethod
     def gen_whitespace(wsps):
         for wsp in wsps:
-            tags.span(wsp, cls="coq-wsp")
+            tags.span(wsp, cls="alectryon-wsp")
 
     def gen_sentence(self, fr):
         if fr.contents is not None:
             self.gen_whitespace(fr.prefixes)
-        with tags.span(cls="coq-sentence"):
+        with tags.span(cls="alectryon-sentence"):
             toggle = self.gen_input_toggle(fr)
             if fr.contents is not None:
                 self.gen_input(fr, toggle)
@@ -186,8 +186,8 @@ def gen_sentence(self, fr):
                 self.gen_whitespace(fr.suffixes)
 
     def gen_fragment(self, fr):
-        if isinstance(fr, CoqText):
-            tags.span(self.highlight(fr.contents), cls="coq-wsp")
+        if isinstance(fr, Text):
+            tags.span(self.highlight(fr.contents), cls="alectryon-wsp")
         else:
             assert isinstance(fr, RichSentence)
             self.gen_sentence(fr)

alectryon/json.py

@@ -24,29 +24,29 @@
 
 from . import core
 
-COQ_TYPE_OF_ALIASES = {
-    "text": core.CoqText,
-    "hypothesis": core.CoqHypothesis,
-    "goal": core.CoqGoal,
-    "message": core.CoqMessage,
-    "sentence": core.CoqSentence,
-    "goals": core.CoqGoals,
-    "messages": core.CoqMessages,
+TYPE_OF_ALIASES = {
+    "text": core.Text,
+    "hypothesis": core.Hypothesis,
+    "goal": core.Goal,
+    "message": core.Message,
+    "sentence": core.Sentence,
+    "goals": core.Goals,
+    "messages": core.Messages,
     "rich_sentence": core.RichSentence,
 }
 
-ALIASES_OF_COQ_TYPE = {
-    cls.__name__: alias for (alias, cls) in COQ_TYPE_OF_ALIASES.items()
+ALIASES_OF_TYPE = {
+    cls.__name__: alias for (alias, cls) in TYPE_OF_ALIASES.items()
 }
 
-COQ_TYPES = list(COQ_TYPE_OF_ALIASES.values())
+TYPES = list(TYPE_OF_ALIASES.values())
 
 def json_of_annotated(obj):
     if isinstance(obj, list):
         return [json_of_annotated(x) for x in obj]
     if isinstance(obj, dict):
         return {k: json_of_annotated(v) for k, v in obj.items()}
-    type_name = ALIASES_OF_COQ_TYPE.get(type(obj).__name__)
+    type_name = ALIASES_OF_TYPE.get(type(obj).__name__)
     if type_name:
         d = {"_type": type_name}
         for k, v in zip(obj._fields, obj):
@@ -60,9 +60,9 @@ def minimal_json_of_annotated(obj):
         return [minimal_json_of_annotated(x) for x in obj]
     if isinstance(obj, dict):
         return {k: minimal_json_of_annotated(v) for k, v in obj.items()}
-    type_name = ALIASES_OF_COQ_TYPE.get(type(obj).__name__)
+    type_name = ALIASES_OF_TYPE.get(type(obj).__name__)
     if type_name:
-        if isinstance(obj, core.CoqText):
+        if isinstance(obj, core.Text):
             return obj.contents
         d = {k: minimal_json_of_annotated(v) for k, v in zip(obj._fields, obj)}
         contents = d.pop("contents", None)
@@ -77,12 +77,12 @@ def annotated_of_json(js):
         return [annotated_of_json(x) for x in js]
     if isinstance(js, dict):
         type_name = js.get("_type")
-        type_constr = COQ_TYPE_OF_ALIASES.get(type_name)
-        coq = {k: annotated_of_json(v) for k, v in js.items()}
+        type_constr = TYPE_OF_ALIASES.get(type_name)
+        obj = {k: annotated_of_json(v) for k, v in js.items()}
         if type_constr:
-            del coq["_type"]
-            return type_constr(**coq)
-        return coq
+            del obj["_type"]
+            return type_constr(**obj)
+        return obj
     return js
 
 def validate_inputs(annotated, reference):
@@ -92,7 +92,7 @@ def validate_inputs(annotated, reference):
             return False
         return all(validate_inputs(*p) for p in zip_longest(annotated, reference))
     # pylint: disable=isinstance-second-argument-not-valid-type
-    if isinstance(annotated, COQ_TYPES):
+    if isinstance(annotated, TYPES):
         if annotated.contents != reference:
             print(f"Mismatch: {annotated.contents} {reference}")
         return annotated.contents == reference

alectryon/latex.py

@@ -20,7 +20,7 @@
 
 import re
 
-from .core import CoqText, RichSentence, CoqMessages, CoqGoals
+from .core import Text, RichSentence, Messages, Goals
 from . import transforms, GENERATOR
 
 def format_macro(name, args, optargs):
@@ -54,7 +54,7 @@ def claim(self, *children):
 
     def add(self, child):
         if isinstance(child, str):
-            child = Text(child)
+            child = PlainText(child)
         self.children.append(child)
         self.claim(child)
 
@@ -135,7 +135,7 @@ def raw_format(cls, tex, indent, verbatim):
     def format(self, indent, verbatim):
         return self.raw_format(self.s, indent, verbatim)
 
-class Text(Raw):
+class PlainText(Raw):
     ESCAPES = Replacements({"\\": "\\bsl"}) # FIXME # Use pygments directly?
 
     def format(self, indent, verbatim):
@@ -177,7 +177,7 @@ def gen_goals(self, first, more):
     def gen_whitespace(wsps):
         # Unlike in HTML, we don't need a separate wsp environment
         for wsp in wsps:
-            yield Text(wsp)
+            yield PlainText(wsp)
 
     def gen_input(self, fr):
         contents = []
@@ -195,12 +195,12 @@ def gen_input(self, fr):
     def gen_output(self, fr):
         with environments.output():
             for output in fr.outputs:
-                if isinstance(output, CoqMessages):
+                if isinstance(output, Messages):
                     assert output.messages, "transforms.commit_io_annotations"
                     with environments.messages():
                         for message in output.messages:
                             environments.message(*self.highlight(message.contents), verbatim=True)
-                if isinstance(output, CoqGoals):
+                if isinstance(output, Goals):
                     assert output.goals, "transforms.commit_io_annotations"
                     with environments.goals():
                         self.gen_goals(output.goals[0], output.goals[1:])
@@ -213,7 +213,7 @@ def gen_sentence(self, fr):
                 self.gen_output(fr)
 
     def gen_fragment(self, fr):
-        if isinstance(fr, CoqText):
+        if isinstance(fr, Text):
             if fr.contents:
                 environments.txt(*self.highlight(fr.contents), verbatim=True)
         else: