Email Gateway (Aug 22 2022 at 08:58): Email Gateway (Aug 22 2022 at 08:58):From: "W. Douglas Maurer" <maurer@gwu.edu>
OK. I see the problem now. The problem is that at one point I
was told that, >>> when searching Isabelle/Isar documentation for
something including an >>> underscore, I have to substitute a
hyphen. Now I find that this is sometimes >>> true and sometimes
not. For "Isabelle/HOL -- Higher-Order Logic," it is true; >>> for
"Isabelle/Isar Reference Manual," it's apparently not true. I was
searching for case-names when I should have been searching for
case_names. >> PDF is electronic paper, with some uncertainty of
real paper. Some PDF viewers >> also use OCR to find things, but you
never know 100% what it is. >> To make really sure, you
can always search the formal sources in
$ISABELLE_HOME/src/Doc/Isar_Ref/.
<snip>
Talking about source files I was referring to the default Isabelle
source editor,
which is Isabelle/jEdit. The above $ISABELLE_HOME/src/Doc/Isar_Ref works
literally in its file-dialog, even on Windows.
<snip>
Makarius
When I search the PDF file "Isabelle/Isar Reference Manual," it
searches the whole manual, which is what I want. I want to see
whether certain terms appear anywhere in that manual (sometimes
they don't). When I bring up $ISABELLE_HOME/src/Doc/Isar_Ref in the
file-dialog of Isabelle/jEdit, I don't get a file which is the whole
manual. Instead I get 16 files, from Base.thy through Synopsis.thy .
To do my search, it would seem that I have to search each one of
these separately, and that appears tedious. The same problem happens
when I try to search "Isabelle/HOL -- Higher-Order Logic." I can
search the PDF file to see whether a term appears there anywhere; but
searching the formal sources would seem to involve several dozen
files separately. Is there, anywhere, a single formal source for all
of "Isabelle/Isar Reference Manual," and/or a single formal source
for all of "Isabelle/HOL -- Higher-Order Logic"? Thanks! -Douglas
Email Gateway (Aug 22 2022 at 08:58):From: Larry Paulson <lp15@cam.ac.uk>
Under UNIX, you might want to try
grep blah -r Doc/Isar_Ref
or whatever. It’s often useful. Also, many editors can be set to search entire directories.
Larry Paulson
Email Gateway (Aug 22 2022 at 08:58):From: Makarius <makarius@sketis.net>
jEdit is particulary good at this -- its search dialog (with hypersearch)
is one of the things why I gave up Emacs and command lines as above in
2006.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC