src/Pure/ML-Systems/ml_parse_tree.ML
author wenzelm
Fri, 17 Jul 2015 16:23:25 +0200
changeset 60744 4eba53a0ac3d
parent 60731 4ac4b314d93c
permissions -rw-r--r--
report possible breakpoint positions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;