isabelle: src/Pure/ML-Systems/ml_parse_tree.ML@abe08fb15a12 (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.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.
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	wenzelm
	Fri, 25 Sep 2015 20:37:59 +0200
changeset 61268	abe08fb15a12
parent 60744	4eba53a0ac3d
permissions	-rw-r--r--