failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
## targets
default: Sugar
images:
test: Sugar
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document -M 1
## Sugar
Sugar: $(LOG)/HOL-Sugar.gz
$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/Sugar.thy \
Sugar/document/root.tex Sugar/document/root.bib \
$(SRC)/HOL/Library/LaTeXsugar.thy $(SRC)/HOL/Library/OptionalSugar.thy
@$(USEDIR) HOL Sugar
@rm -f Sugar/document/isabelle.sty Sugar/document/isabellesym.sty \
Sugar/document/pdfsetup.sty Sugar/document/session.tex
## clean
clean:
@rm -f $(LOG)/HOL-Sugar.gz