# HG changeset patch
# User wenzelm
# Date 1459517545 -7200
# Node ID 374820748c70673777e5f4fe816096c1705403b9
# Parent  f90a9fe3329fa2eb4e2bbb7ab4d6f84b5f1930ef
unused;

diff -r f90a9fe3329f -r 374820748c70 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Apr 01 15:27:59 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Apr 01 15:32:25 2016 +0200
@@ -66,10 +66,10 @@
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
-  val markupN: string val get_markup: Properties.T -> string
-  val consistentN: string val get_consistent: Properties.T -> bool
+  val markupN: string
+  val consistentN: string
   val block_properties: string list
-  val indentN: string val get_indent: Properties.T -> int
+  val indentN: string
   val widthN: string
   val blockN: string val block: bool -> int -> T
   val breakN: string val break: int -> int -> T
@@ -401,14 +401,6 @@
 
 val block_properties = [markupN, consistentN, indentN];
 
-fun get_markup props = the_default "" (Properties.get props markupN);
-
-fun get_consistent props =
-  the_default false (Option.map parse_bool (Properties.get props consistentN));
-
-fun get_indent props =
-  the_default 0 (Option.map parse_int (Properties.get props indentN));
-
 val widthN = "width";
 
 val blockN = "block";