isabelle: src/Pure/RAW/ml_parse_tree.ML@eca7b38c8ee5 (annotated)

62058 1cfd5d604937 updated headers; wenzelm parents: 61925 diff changeset	1	(* Title: Pure/RAW/ml_parse_tree.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
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.
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	signature ML_PARSE_TREE =
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	8	sig
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	9	val completions: PolyML.ptProperties -> string list option
60744 4eba53a0ac3d report possible breakpoint positions; wenzelm parents: 60731 diff changeset	10	val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
60731 4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	11	end;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	12
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	13	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	14	struct
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	fun completions _ = NONE;
60744 4eba53a0ac3d report possible breakpoint positions; wenzelm parents: 60731 diff changeset	17	fun breakpoint _ = NONE;
60731 4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	18
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later; wenzelm parents: diff changeset	19	end;

author	Manuel Eberl <eberlm@in.tum.de>
	Tue, 19 Jan 2016 11:19:25 +0100
changeset 62201	eca7b38c8ee5
parent 62058	1cfd5d604937
permissions	-rw-r--r--