src/Pure/PIDE/markup.ML
changeset 50500 c94bba7906d2
parent 50499 f496b2b7bafb
child 50503 50f141b34bb7
     1.1 --- a/src/Pure/PIDE/markup.ML	Wed Dec 12 23:36:07 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Thu Dec 13 13:52:18 2012 +0100
     1.3 @@ -96,12 +96,6 @@
     1.4    val proof_stateN: string val proof_state: int -> T
     1.5    val stateN: string val state: T
     1.6    val subgoalN: string val subgoal: T
     1.7 -  val graphviewN: string
     1.8 -  val sendbackN: string
     1.9 -  val paddingN: string
    1.10 -  val padding_line: string * string
    1.11 -  val dialogN: string val dialog: string -> string -> T
    1.12 -  val intensifyN: string val intensify: T
    1.13    val taskN: string
    1.14    val acceptedN: string val accepted: T
    1.15    val forkedN: string val forked: T
    1.16 @@ -122,6 +116,12 @@
    1.17    val reportN: string val report: T
    1.18    val no_reportN: string val no_report: T
    1.19    val badN: string val bad: T
    1.20 +  val intensifyN: string val intensify: T
    1.21 +  val graphviewN: string
    1.22 +  val sendbackN: string
    1.23 +  val paddingN: string
    1.24 +  val padding_line: string * string
    1.25 +  val dialogN: string val dialog: serial -> string -> T
    1.26    val functionN: string
    1.27    val assign_execs: Properties.T
    1.28    val removed_versions: Properties.T
    1.29 @@ -339,20 +339,6 @@
    1.30  val (subgoalN, subgoal) = markup_elem "subgoal";
    1.31  
    1.32  
    1.33 -(* active areas *)
    1.34 -
    1.35 -val graphviewN = "graphview";
    1.36 -
    1.37 -val sendbackN = "sendback";
    1.38 -val paddingN = "padding";
    1.39 -val padding_line = (paddingN, lineN);
    1.40 -
    1.41 -val dialogN = "dialog";
    1.42 -fun dialog name result = (dialogN, [(nameN, name), ("result", result)]);
    1.43 -
    1.44 -val (intensifyN, intensify) = markup_elem "intensify";
    1.45 -
    1.46 -
    1.47  (* command status *)
    1.48  
    1.49  val taskN = "task";
    1.50 @@ -385,6 +371,20 @@
    1.51  
    1.52  val (badN, bad) = markup_elem "bad";
    1.53  
    1.54 +val (intensifyN, intensify) = markup_elem "intensify";
    1.55 +
    1.56 +
    1.57 +(* active areas *)
    1.58 +
    1.59 +val graphviewN = "graphview";
    1.60 +
    1.61 +val sendbackN = "sendback";
    1.62 +val paddingN = "padding";
    1.63 +val padding_line = (paddingN, lineN);
    1.64 +
    1.65 +val dialogN = "dialog";
    1.66 +fun dialog i result = (dialogN, [(serialN, print_int i), ("result", result)]);
    1.67 +
    1.68  
    1.69  (* protocol message functions *)
    1.70