isabelle: src/Pure/RAW/ml_parse_tree_polyml-5.6.ML@eca7b38c8ee5 (annotated)

61925 ab52f183f020 clarified directory structure; wenzelm parents: 61794 diff changeset	1	(* Title: Pure/RAW/ml_parse_tree_polyml-5.6.ML
60731 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
61794 4c232a2ddeab discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6; wenzelm parents: 60744 diff changeset	4	Additional ML parse tree components for Poly/ML 5.6, or later.
60731 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	Manuel Eberl <eberlm@in.tum.de>
	Tue, 19 Jan 2016 11:19:25 +0100
changeset 62201	eca7b38c8ee5
parent 61925	ab52f183f020
permissions	-rw-r--r--