[isabelle-dev] Purpose of guess_infix

[Florian Haftmann]

Hi Makarius,

I guess this had something to do with Haskabelle, taking into account
its fundamental design flaw to write terms on its own rather than having
Isabelle's existing printing doing the job.

Since there is no reference left, it can be safely discarded.

Cheers,
	Florian

Am 15.09.2018 um 21:32 schrieb Makarius:
> What is the purpose of guess_infix? It appears to be unused in current
> Isabelle/10da16970d82.
> 
> It orgininates from the following changeset:
> 
> changeset:   26678:a3ae088dc20f
> user:        haftmann
> date:        Wed Apr 16 10:50:37 2008 +0200
> files:       src/Pure/Syntax/parser.ML src/Pure/Syntax/syntax.ML
> description:
> educated guess for infix syntax
> 
> 
> The motivation behind the question: slightly more high-level access to
> notation, e.g. for export to other languages; possibly without "fishing"
> in the generated grammar.
> 
> 
> 	Makarius
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180916/78b52714/attachment.sig>