# HG changeset patch # User wenzelm # Date 1377853469 -7200 # Node ID c3e549e0d3c75a0d8db1fb3d2b370d0710a168f3 # Parent b102e20cec786be910012bb429f35fb3a23dd4e4 allow multiple symbol properties, notably groups and abbrevs; diff -r b102e20cec78 -r c3e549e0d3c7 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Aug 30 11:00:46 2013 +0200 +++ b/src/Pure/General/symbol.scala Fri Aug 30 11:04:29 2013 +0200 @@ -216,27 +216,28 @@ private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """) private val Key = new Regex("""(?xs) (.+): """) - private def read_decl(decl: String): (Symbol, Map[String, String]) = + private def read_decl(decl: String): (Symbol, Properties.T) = { def err() = error("Bad symbol declaration: " + decl) - def read_props(props: List[String]): Map[String, String] = + def read_props(props: List[String]): Properties.T = { props match { - case Nil => Map() + case Nil => Nil case _ :: Nil => err() - case Key(x) :: y :: rest => read_props(rest) + (x -> y) + case Key(x) :: y :: rest => (x -> y) :: read_props(rest) case _ => err() } } decl.split("\\s+").toList match { - case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props)) + case sym :: props if sym.length > 1 && !is_malformed(sym) => + (sym, read_props(props)) case _ => err() } } - private val symbols: List[(Symbol, Map[String, String])] = - (((List.empty[(Symbol, Map[String, String])], Set.empty[Symbol]) /: + private val symbols: List[(Symbol, Properties.T)] = + (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /: split_lines(symbols_spec).reverse) { case (res, No_Decl()) => res case ((list, known), decl) => @@ -255,28 +256,35 @@ } val groups: List[(String, List[Symbol])] = - symbols.map({ case (sym, props) => (sym, props.getOrElse("group", "unsorted")) }) + symbols.map({ case (sym, props) => + val gs = for (("group", g) <- props) yield g + if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _) + }).flatten .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) }) .sortBy(_._1) - val abbrevs: Map[Symbol, String] = - Map(( - for ((sym, props) <- symbols if props.isDefinedAt("abbrev")) - yield (sym -> props("abbrev"))): _*) + val abbrevs: Multi_Map[Symbol, String] = + Multi_Map(( + for { + (sym, props) <- symbols + ("abbrev", a) <- props.reverse + } yield (sym -> a)): _*) /* recoding */ + private val Code = new Properties.String("code") private val (decoder, encoder) = { val mapping = for { (sym, props) <- symbols code = - try { Integer.decode(props("code")).intValue } - catch { - case _: NoSuchElementException => error("Missing code for symbol " + sym) - case _: NumberFormatException => error("Bad code for symbol " + sym) + props match { + case Code(s) => + try { Integer.decode(s).intValue } + catch { case _: NumberFormatException => error("Bad code for symbol " + sym) } + case _ => error("Missing code for symbol " + sym) } ch = new String(Character.toChars(code)) } yield { @@ -305,10 +313,9 @@ /* user fonts */ + private val Font = new Properties.String("font") val fonts: Map[Symbol, String] = - recode_map(( - for ((sym, props) <- symbols if props.isDefinedAt("font")) - yield (sym -> props("font"))): _*) + recode_map((for ((sym, Font(font)) <- symbols) yield (sym -> font)): _*) val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*) @@ -376,7 +383,7 @@ def names: Map[Symbol, String] = symbols.names def groups: List[(String, List[Symbol])] = symbols.groups - def abbrevs: Map[Symbol, String] = symbols.abbrevs + def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs def decode(text: String): String = symbols.decode(text) def encode(text: String): String = symbols.encode(text) diff -r b102e20cec78 -r c3e549e0d3c7 src/Pure/Isar/completion.scala --- a/src/Pure/Isar/completion.scala Fri Aug 30 11:00:46 2013 +0200 +++ b/src/Pure/Isar/completion.scala Fri Aug 30 11:04:29 2013 +0200 @@ -74,10 +74,10 @@ val words = (for ((x, _) <- Symbol.names) yield (x, x)).toList ::: (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList ::: - (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList + (for ((x, y) <- Symbol.abbrevs.iterator if Completion.is_word(y)) yield (y, x)).toList val abbrs = - (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y)) + (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.is_word(y)) yield (y.reverse.toString, (y, x))).toList new Completion( diff -r b102e20cec78 -r c3e549e0d3c7 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Aug 30 11:00:46 2013 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Aug 30 11:04:29 2013 +0200 @@ -43,8 +43,7 @@ } tooltip = JEdit_Lib.wrap_tooltip( - symbol + - (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else "")) + cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))) } private class Reset_Component extends Button