[ProofPower] Font for SML

[David Topham]

I am exploring a not often used but nice Latex package named ffslides. It
has several advantages in exact control of where things are placed on the
page using postscript (actually pstricks) behind the scenes. But, one
problem is that the SML in my doc file is getting scrunched together like
this:

*funsubset([],[])=true*

Is there a way for me to choose a different font when doctex extracts the
SML?
Maybe I could find an alternative that would not squash?

-Dave


,
[])=
true

[Roger Bishop Jones]

David,

Doctex doesn't chose a font, it just generates LaTeX commands for the
formal text and any font changing is up to the rest of the document
(that you provide in the =TEX sections of the .doc file).

It does generate tex for the HOL and ZED paragraphs which is intended to
force the layout in the printed version to follow the layout in the
source, which tex would not normally do, so I guess the ffslides package
is interfering with the way that works.
The formal text is translated into tex using an environment GFT which is
defined in ProofPower.sty, but its beyond my tex expertise to understand
how it works or why ffslides is interfering.

It is possible to get slides made with ProofPower formal text in them,
the tutorial slides in the ProofPower distribution are examples of how
this can be done, though the method used for them is probably rather
ancient by now.

Roger

Post by David Topham
I am exploring a not often used but nice Latex package named ffslides.
It has several advantages in exact control of where things are placed
on the page using postscript (actually pstricks) behind the scenes.
But, one problem is that the SML in my doc file is getting scrunched
/funsubset([],[])=true/
/
/
Is there a way for me to choose a different font when doctex extracts
the SML?
Maybe I could find an alternative that would not squash?
-Dave
,
[])=
true
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[David Topham]

Thanks Roger, In case you wish to see the problem more exactly attached is
the doc file and the ffslides.cls (which you could also get at CTAN). It
seems that for SML, the spaces are all removed! I will look into GFT to
see how spaces are inserted. One issue might be if verbatim environment is
used? -Dave

Post by Roger Bishop Jones
David,
Doctex doesn't chose a font, it just generates LaTeX commands for the
formal text and any font changing is up to the rest of the document (that
you provide in the =TEX sections of the .doc file).
It does generate tex for the HOL and ZED paragraphs which is intended to
force the layout in the printed version to follow the layout in the source,
which tex would not normally do, so I guess the ffslides package is
interfering with the way that works.
The formal text is translated into tex using an environment GFT which is
defined in ProofPower.sty, but its beyond my tex expertise to understand
how it works or why ffslides is interfering.
It is possible to get slides made with ProofPower formal text in them, the
tutorial slides in the ProofPower distribution are examples of how this can
be done, though the method used for them is probably rather ancient by now.
Roger
I am exploring a not often used but nice Latex package named ffslides. It
has several advantages in exact control of where things are placed on the
page using postscript (actually pstricks) behind the scenes. But, one
problem is that the SML in my doc file is getting scrunched together like
*funsubset([],[])=true*
Is there a way for me to choose a different font when doctex extracts the
SML?
Maybe I could find an alternative that would not squash?
-Dave
,
[])=
true
_______________________________________________
------------------------------
This message did not originate from Ohlone College and must be viewed with
caution. Viruses and phishing attempts can be transmitted via email. E-mail
transmission cannot be guaranteed to be secure or error-free as information
could be intercepted, corrupted, lost, destroyed, arrive late or
incomplete, or contain viruses. If you have any concerns, please contact
659-7333.

[David Topham]

...forgot to mention...need to go through postscript, so
latex lab.tex
dvipdf lab.dvi

Post by David Topham
Thanks Roger, In case you wish to see the problem more exactly attached is
the doc file and the ffslides.cls (which you could also get at CTAN). It
seems that for SML, the spaces are all removed! I will look into GFT to
see how spaces are inserted. One issue might be if verbatim environment is
used? -Dave

Post by Roger Bishop Jones
David,
Doctex doesn't chose a font, it just generates LaTeX commands for the
formal text and any font changing is up to the rest of the document (that
you provide in the =TEX sections of the .doc file).
It does generate tex for the HOL and ZED paragraphs which is intended to
force the layout in the printed version to follow the layout in the source,
which tex would not normally do, so I guess the ffslides package is
interfering with the way that works.
The formal text is translated into tex using an environment GFT which is
defined in ProofPower.sty, but its beyond my tex expertise to understand
how it works or why ffslides is interfering.
It is possible to get slides made with ProofPower formal text in them,
the tutorial slides in the ProofPower distribution are examples of how this
can be done, though the method used for them is probably rather ancient by
now.
Roger
I am exploring a not often used but nice Latex package named ffslides. It
has several advantages in exact control of where things are placed on the
page using postscript (actually pstricks) behind the scenes. But, one
problem is that the SML in my doc file is getting scrunched together like
*funsubset([],[])=true*
Is there a way for me to choose a different font when doctex extracts the
SML?
Maybe I could find an alternative that would not squash?
-Dave
,
[])=
true
_______________________________________________
------------------------------
This message did not originate from Ohlone College and must be viewed
with caution. Viruses and phishing attempts can be transmitted via email.
E-mail transmission cannot be guaranteed to be secure or error-free as
information could be intercepted, corrupted, lost, destroyed, arrive late
or incomplete, or contain viruses. If you have any concerns, please contact
659-7333.

[Rob Arthan]

David,

The ProofPower environments use \obeyspaces to persuade LaTeX to honour the spaces
in ML code etc. The ffslides package is doing something that is stopping \obeyspaces
working properly. A quick fix would be to edit the .tex file (lab.tex in your example) to replace
spaces between \begin{GFT} and \end{GFT} with tildes.

Regards,

Rob.

Post by David Topham
...forgot to mention...need to go through postscript, so
latex lab.tex
dvipdf lab.dvi
Thanks Roger, In case you wish to see the problem more exactly attached is the doc file and the ffslides.cls (which you could also get at CTAN). It seems that for SML, the spaces are all removed! I will look into GFT to see how spaces are inserted. One issue might be if verbatim environment is used? -Dave
David,
Doctex doesn't chose a font, it just generates LaTeX commands for the formal text and any font changing is up to the rest of the document (that you provide in the =TEX sections of the .doc file).
It does generate tex for the HOL and ZED paragraphs which is intended to force the layout in the printed version to follow the layout in the source, which tex would not normally do, so I guess the ffslides package is interfering with the way that works.
The formal text is translated into tex using an environment GFT which is defined in ProofPower.sty, but its beyond my tex expertise to understand how it works or why ffslides is interfering.
It is possible to get slides made with ProofPower formal text in them, the tutorial slides in the ProofPower distribution are examples of how this can be done, though the method used for them is probably rather ancient by now.
Roger

Post by David Topham
funsubset([],[])=true
Is there a way for me to choose a different font when doctex extracts the SML?
Maybe I could find an alternative that would not squash?
-Dave
,
[])=
true
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com <http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>

_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[David Topham]

Rob, That idea does work: when I replace all spaces with ~ I get good
output. I would need to post-process each tex file though. Maybe I can
work out a script to do that and integrate it with docdvi (as Roger
suggested)? First I will try to see if/how ffslides may be interfering with
obeyspaces. I did read in the ffslides documentation that we can't use
verbatim directly since pstricks (postscript) has some problem with that.
Maybe a related issue.
Thanks for the tip; that is a good work-around for now. -Dave

Post by Roger Bishop Jones
David,
The ProofPower environments use \obeyspaces to persuade LaTeX to honour the spaces
in ML code etc. The ffslides package is doing something that is stopping \obeyspaces
working properly. A quick fix would be to edit the .tex file (lab.tex in
your example) to replace
spaces between \begin{GFT} and \end{GFT} with tildes.
Regards,
Rob.
...forgot to mention...need to go through postscript, so
latex lab.tex
dvipdf lab.dvi

Post by David Topham
Thanks Roger, In case you wish to see the problem more exactly attached
is the doc file and the ffslides.cls (which you could also get at CTAN).
It seems that for SML, the spaces are all removed! I will look into GFT to
see how spaces are inserted. One issue might be if verbatim environment is
used? -Dave

Post by Roger Bishop Jones
David,
Doctex doesn't chose a font, it just generates LaTeX commands for the
formal text and any font changing is up to the rest of the document (that
you provide in the =TEX sections of the .doc file).
It does generate tex for the HOL and ZED paragraphs which is intended to
force the layout in the printed version to follow the layout in the source,
which tex would not normally do, so I guess the ffslides package is
interfering with the way that works.
The formal text is translated into tex using an environment GFT which is
defined in ProofPower.sty, but its beyond my tex expertise to understand
how it works or why ffslides is interfering.
It is possible to get slides made with ProofPower formal text in them,
the tutorial slides in the ProofPower distribution are examples of how this
can be done, though the method used for them is probably rather ancient by
now.
Roger
I am exploring a not often used but nice Latex package named ffslides.
It has several advantages in exact control of where things are placed on
the page using postscript (actually pstricks) behind the scenes. But, one
problem is that the SML in my doc file is getting scrunched together like
*funsubset([],[])=true*
Is there a way for me to choose a different font when doctex extracts the SML?
Maybe I could find an alternative that would not squash?
-Dave
,
[])=
true
_______________________________________________
------------------------------
This message did not originate from Ohlone College and must be viewed
with caution. Viruses and phishing attempts can be transmitted via email.
E-mail transmission cannot be guaranteed to be secure or error-free as
information could be intercepted, corrupted, lost, destroyed, arrive late
or incomplete, or contain viruses. If you have any concerns, please contact
659-7333.

_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[David Topham]

Rob,
The author of the Latex class ffslides (Mark Wolters) suggested I try
putting \obeyspaces right at top line of \begin{document} and that works!
Great! All the SML is now spaced correctly. That means I don't have to
post-process the tex file. It remains
to be seen if that breaks anything else, but so far it is fine.
Thanks for the tip! -Dave

Post by David Topham
Rob, That idea does work: when I replace all spaces with ~ I get good
output. I would need to post-process each tex file though. Maybe I can
work out a script to do that and integrate it with docdvi (as Roger
suggested)? First I will try to see if/how ffslides may be interfering with
obeyspaces. I did read in the ffslides documentation that we can't use
verbatim directly since pstricks (postscript) has some problem with that.
Maybe a related issue.
Thanks for the tip; that is a good work-around for now. -Dave

Post by Roger Bishop Jones
David,
The ProofPower environments use \obeyspaces to persuade LaTeX to honour the spaces
in ML code etc. The ffslides package is doing something that is stopping \obeyspaces
working properly. A quick fix would be to edit the .tex file (lab.tex in
your example) to replace
spaces between \begin{GFT} and \end{GFT} with tildes.
Regards,
Rob.
...forgot to mention...need to go through postscript, so
latex lab.tex
dvipdf lab.dvi

Post by David Topham
Thanks Roger, In case you wish to see the problem more exactly attached
is the doc file and the ffslides.cls (which you could also get at CTAN).
It seems that for SML, the spaces are all removed! I will look into GFT to
see how spaces are inserted. One issue might be if verbatim environment is
used? -Dave

Post by Roger Bishop Jones
David,
Doctex doesn't chose a font, it just generates LaTeX commands for the
formal text and any font changing is up to the rest of the document (that
you provide in the =TEX sections of the .doc file).
It does generate tex for the HOL and ZED paragraphs which is intended
to force the layout in the printed version to follow the layout in the
source, which tex would not normally do, so I guess the ffslides package is
interfering with the way that works.
The formal text is translated into tex using an environment GFT which
is defined in ProofPower.sty, but its beyond my tex expertise to understand
how it works or why ffslides is interfering.
It is possible to get slides made with ProofPower formal text in them,
the tutorial slides in the ProofPower distribution are examples of how this
can be done, though the method used for them is probably rather ancient by
now.
Roger
I am exploring a not often used but nice Latex package named ffslides.
It has several advantages in exact control of where things are placed on
the page using postscript (actually pstricks) behind the scenes. But, one
problem is that the SML in my doc file is getting scrunched together like
*funsubset([],[])=true*
Is there a way for me to choose a different font when doctex extracts the SML?
Maybe I could find an alternative that would not squash?
-Dave
,
[])=
true
_______________________________________________
------------------------------
This message did not originate from Ohlone College and must be viewed
with caution. Viruses and phishing attempts can be transmitted via email.
E-mail transmission cannot be guaranteed to be secure or error-free as
information could be intercepted, corrupted, lost, destroyed, arrive late
or incomplete, or contain viruses. If you have any concerns, please contact
659-7333.

_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[Roger Bishop Jones]

David,

Looks like one problem for you is the way you are processing the latex
files.

There is a ProofPower manual, USR001, called:ProofPower - Document
Preparation <http://www.lemma-one.com/ProofPower/doc/usr001.pdf>
which tells you how to process ProofPower files for printing (or to .dvi
files).
Rather than converting to .tex and then running latex on the tex file,
you should be
using docdvi, which will extract the .tex file and run it through LaTeX
for you.

I could not check this out for you because I was still short of a style
file pstricks.sty
so I can't be sure that would work for your document, but you should try
it yourself
and see how it goes.

Roger