src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML
author wenzelm
Wed, 12 Aug 2015 13:53:51 +0200
changeset 60916 a6e2a667b0a8
parent 60744 4eba53a0ac3d
permissions -rw-r--r--
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
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_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;