Re: [ProofPower] Font for SML

2016-10-05 Thread 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

Re: [ProofPower] Font for SML

2016-10-05 Thread 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 u

Re: [ProofPower] Font for SML

2016-10-05 Thread David Topham
...forgot to mention...need to go through postscript, so latex lab.tex dvipdf lab.dvi On Wed, Oct 5, 2016 at 12:28 PM, David Topham wrote: > 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 > s

Re: [ProofPower] Font for SML

2016-10-05 Thread 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{

Re: [ProofPower] Font for SML

2016-10-05 Thread 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 which tells you how to process ProofPower files for printing (or to .dvi fi

Re: [ProofPower] Font for SML

2016-10-05 Thread 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 obeyspace