isabelle: src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML@0d4ee4168e41 (annotated)

60731 4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	1	(* Title: Pure/ML/ml_parse_tree_polyml-5.5.3.ML
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	2	Author: Makarius
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	3
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	4	Additional ML parse tree components for Poly/ML 5.5.3, or later.
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	5	*)
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	6
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	7	structure ML_Parse_Tree: ML_PARSE_TREE =
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	8	struct
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	9
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	10	fun completions (PolyML.PTcompletions x) = SOME x
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	11	\| completions _ = NONE;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	12
60744 4eba53a0ac3d report possible breakpoint positions; wenzelm parents: 60731 diff changeset	13	fun breakpoint (PolyML.PTbreakPoint x) = SOME x
4eba53a0ac3d report possible breakpoint positions; wenzelm parents: 60731 diff changeset	14	\| breakpoint _ = NONE;
60731 4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	15
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	16	end;

author	wenzelm
	Tue, 03 Nov 2015 13:54:34 +0100
changeset 61556	0d4ee4168e41
parent 60744	4eba53a0ac3d
permissions	-rw-r--r--