PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
170 stars 28 forks source link

Dependency graph is not properly generated if there is no empty line above '\begin{theorem}' #7

Open ianjauslin-rutgers opened 11 months ago

ianjauslin-rutgers commented 11 months ago

I ran into an issue where the dependency graph is not generated properly if the line preceding '\begin{theorem}' or '\begin{definition}' is not empty.

Setup:

Steps to reproduce: use the following tex file:


\usepackage{amsmath, amsthm}
\usepackage[showmore, dep_graph, coverage, project=../../]{blueprint}

\newtheorem{theorem}{Theorem}

\begin{document}

tt
\begin{theorem}
  \label{tt:test}
  Test
\end{theorem}

\begin{proof}
test
\end{proof}

tt
\begin{theorem}
  \label{tt:test2}
  Test
\end{theorem}

\begin{proof}
\uses{tt:test}
test uses \ref{tt:test}
\end{proof}

\end{document}

The dependency graph does not show the dependency between test and test2. It works fine if the lines before the theorems are blank.

SriAR commented 10 months ago

My codebase is horribly mangled so I cannot submit a PR for this right now, but one fix is to change

https://github.com/PatrickMassot/leanblueprint/blob/7ce2f47fc5ed955b4d473e8c14d93ea702ad4c48/leanblueprint/Packages/blueprint.py#L321-L322

to

        if childNodes:
            for grandchildNode in childNodes:
                if grandchildNode.nodeName == 'thmenv':
                    return grandchildNode
PatrickMassot commented 10 months ago

Could you please test again with plastex's master branch? I pushed a fix there which should be relevant.

PatrickMassot commented 10 months ago

Correction: I realized my "fix" was incorrect so I reverted it. Sorry about the noise. I will continue to investigate.

PatrickMassot commented 10 months ago

It should be good now.